Merge pull request #3795 from peterschrammel/multi-path-symex-checker

Multi-path symex checker [blocks: 3796]

Author: peterschrammel

jbmc/src/java_bytecode/java_multi_path_symex_checker.h

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: Goto Checker using Bounded Model Checking for Java
+
+Author: Daniel Kroening, Peter Schrammel
+
+ \*******************************************************************/
+
+/// \file
+/// Goto Checker using Bounded Model Checking for Java
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H
+#define CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H
+
+#include <goto-checker/multi_path_symex_checker.h>
+
+#include "java_bmc_util.h"
+
+class java_multi_path_symex_checkert : public multi_path_symex_checkert
+{
+public:
+  java_multi_path_symex_checkert(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler,
+    abstract_goto_modelt &goto_model)
+    : multi_path_symex_checkert(options, ui_message_handler, goto_model)
+  {
+    java_setup_symex(options, goto_model, symex);
+  }
+};
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H

jbmc/src/jbmc/Makefile

@@ -41,7 +41,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
       # Empty last line
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
 #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-programs/adjust_float_expressions.h>
 #include <goto-programs/lazy_goto_model.h>
@@ -61,6 +62,7 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/convert_java_nondet.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
+#include <java_bytecode/java_multi_path_symex_checker.h>
 #include <java_bytecode/java_multi_path_symex_only_checker.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
@@ -564,13 +566,30 @@ int jbmc_parse_optionst::doit()
       }
     }
 
-    // The `configure_bmc` callback passed will enable enum-unwind-static if
-    // applicable.
-    return bmct::do_language_agnostic_bmc(
-      options,
-      goto_model,
-      ui_message_handler,
-      configure_bmc);
+    std::unique_ptr<goto_verifiert> verifier = nullptr;
+
+    if(!options.get_bool_option("paths") && !options.is_set("cover"))
+    {
+      if(!options.get_bool_option("stop-on-fail"))
+      {
+        verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
+          java_multi_path_symex_checkert>>(
+          options, ui_message_handler, goto_model);
+      }
+    }
+
+    // fall back until everything has been ported to goto-checker
+    if(verifier == nullptr)
+    {
+      // The `configure_bmc` callback passed will enable enum-unwind-static if
+      // applicable.
+      return bmct::do_language_agnostic_bmc(
+        options, goto_model, ui_message_handler, configure_bmc);
+    }
+
+    resultt result = (*verifier)();
+    verifier->report();
+    return result_to_exit_code(result);
   }
   else
   {

jbmc/unit/Makefile

@@ -86,7 +86,6 @@ BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/xml_interface$(OBJEXT) \
           $(CPROVER_DIR)/src/jsil/expr2jsil$(OBJEXT) \
@@ -131,6 +130,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \
               $(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
               $(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \
+              $(CPROVER_DIR)/src/assembler/assembler$(LIBEXT) \
               $(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
               $(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \
               $(BMC_DEPS) \

regression/cbmc/Multi_Dimensional_Array6/test.desc

@@ -3,8 +3,8 @@ main.c
 --unwind 3 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.1\] .* : SUCCESS$
-^\[main\.assertion\.2\] .* : FAILURE$
+^\[main\.assertion\.1\] .*: SUCCESS$
+^\[main\.assertion\.2\] .*: FAILURE$
 ^\*\* 1 of 2 failed 
 --
 ^warning: ignoring

regression/cbmc/goto4/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*] line 5 assertion g == 0: SUCCESS$
-^\[.*] unwinding assertion loop 0: FAILURE$
+^\[.*] line 14 unwinding assertion loop 0: FAILURE$
 --
 ^warning: ignoring

regression/contracts/function_check_04/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 --apply-code-contracts
 ^\[main.assertion.1\] .* assertion x == 0: SUCCESS$
-^\[foo.1\] line 9 : FAILURE$
+^\[foo.1\] line 9 .*: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

src/cbmc/Makefile

@@ -4,7 +4,6 @@ SRC = all_properties.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \
       cbmc_parse_options.cpp \
-      counterexample_beautification.cpp \
       fault_localization.cpp \
       xml_interface.cpp \
       # Empty last line

src/cbmc/bmc.cpp

@@ -25,10 +25,10 @@ Author: Daniel Kroening, [email protected]
 #include <linking/static_lifetime_init.h>
 
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/counterexample_beautification.h>
 #include <goto-checker/report_util.h>
 #include <goto-checker/solver_factory.h>
 
-#include "counterexample_beautification.h"
 #include "fault_localization.h"
 
 /// Hook used by CEGIS to selectively freeze variables

src/cbmc/cbmc_parse_options.cpp

@@ -33,7 +33,9 @@ Author: Daniel Kroening, [email protected]
 #include <cpp/cprover_library.h>
 
 #include <goto-checker/all_properties_verifier.h>
+#include <goto-checker/all_properties_verifier_with_trace_storage.h>
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/multi_path_symex_checker.h>
 #include <goto-checker/multi_path_symex_only_checker.h>
 #include <goto-checker/properties.h>
 
@@ -562,8 +564,28 @@ int cbmc_parse_optionst::doit()
     }
   }
 
-  return bmct::do_language_agnostic_bmc(
-    options, goto_model, ui_message_handler);
+  std::unique_ptr<goto_verifiert> verifier = nullptr;
+
+  if(!options.get_bool_option("paths") && !options.is_set("cover"))
+  {
+    if(!options.get_bool_option("stop-on-fail"))
+    {
+      verifier = util_make_unique<
+        all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>>(
+        options, ui_message_handler, goto_model);
+    }
+  }
+
+  // fall back until everything has been ported to goto-checker
+  if(verifier == nullptr)
+  {
+    return bmct::do_language_agnostic_bmc(
+      options, goto_model, ui_message_handler);
+  }
+
+  resultt result = (*verifier)();
+  verifier->report();
+  return result_to_exit_code(result);
 }
 
 bool cbmc_parse_optionst::set_properties()

src/cbmc/fault_localization.cpp

@@ -24,12 +24,13 @@ Author: Peter Schrammel
 #include <solvers/prop/literal_expr.h>
 
 #include <goto-symex/build_goto_trace.h>
+
 #include <goto-programs/xml_goto_trace.h>
 
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/counterexample_beautification.h>
 #include <goto-checker/report_util.h>
 
-#include "counterexample_beautification.h"
 
 void fault_localizationt::freeze_guards()
 {

src/goto-checker/Makefile

@@ -1,6 +1,9 @@
 SRC = bmc_util.cpp \
+      counterexample_beautification.cpp \
       incremental_goto_checker.cpp \
+      goto_trace_storage.cpp \
       goto_verifier.cpp \
+      multi_path_symex_checker.cpp \
       multi_path_symex_only_checker.cpp \
       properties.cpp \
       report_util.cpp \

src/goto-checker/README.md

@@ -0,0 +1,74 @@
+\ingroup module_hidden
+\defgroup goto-checker goto-checker
+
+# Folder goto-checker
+
+\author Peter Schrammel
+
+The \ref goto-checker directory contains interfaces for the verification of
+goto-programs.
+
+There are three main concepts:
+* Property
+* Goto Verifier
+* Incremental Goto Checker
+
+A property has a `property_id` and identifies an assertion that is either
+part of the goto model or generated in the course of executing the verification
+algorithm. A verification algorithm determines the `status` of a property,
+i.e. whether the property has passed verification, failed, is yet to be
+analyzed, etc. See \ref property_infot.
+
+A goto verifier aims at determining and reporting
+the status of all or some of the properties, _independently_ of the
+actual verification algorithm (e.g. path-merging symbolic execution,
+path-wise symbolic execution, abstract interpretation).
+See \ref goto_verifiert.
+
+An incremental goto checker is used by a goto verifier to execute the
+verification algorithm. Incremental goto checkers keep the state of the
+analysis and can be queried by the goto verifier repeatedly to return
+their results incrementally. A query to an incremental goto checker
+either returns when a violated property has been found or the
+verification algorithm has terminated. If a violated property has been
+found then additional information (e.g. a trace) can be retrieved
+from the incremental goto checker (if it supports that).
+See \ref incremental_goto_checkert.
+
+The combination of these three concepts enables:
+* _Verification algorithms can be used interchangeably._
+  There is a single, small interface for our verification engines.
+* _Verification results reporting is uniform across all engines._
+  Downstream tools can use the reporting output without knowing
+  which verification algorithm was at work.
+* _Building variants of verification engines becomes easy._
+  Goto verifier and incremental goto checker implementations are built from
+  small building blocks. It should therefore be easy to build variants
+  by implementing these interfaces instead of hooking into a monolithic engine.
+* _The code becomes easier to maintain._
+  There are N things that do one thing each rather than one thing that does
+  N things. New variants of verification algorithms can be added and removed
+  without impacting others.
+
+There are the following variants of goto verifiers at the moment:
+* \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.
+* \ref all_properties_verifiert : Determines the status of all properties and
+  outputs verification results incrementally. In contrast to
+  \ref all_properties_verifier_with_trace_storaget,
+  \ref all_properties_verifiert does not require to store any traces.
+  A trace ends at a violated property.
+
+There are the following variants of incremental goto checkers at the moment:
+* \ref multi_path_symex_checkert : The default mode of goto-symex. It explores
+  all paths and applies aggressive path merging to generate a formula
+  (aka 'equation') that is passed to the SAT/SMT solver. It supports
+  determining the status of all properties, but not adding new properties
+  after the first invocation.
+* \ref multi_path_symex_only_checkert : Same as \ref multi_path_symex_checkert,
+  but does not call the SAT/SMT solver. It can only decide the status of
+  properties by the simplifications that goto-symex performs.
+* There are variants for Java that perform a Java-specific preprocessing:
+  \ref java_multi_path_symex_checkert,
+  \ref java_multi_path_symex_only_checkert

src/goto-checker/all_properties_verifier.h

@@ -43,19 +43,21 @@ class all_properties_verifiert : public goto_verifiert
           incremental_goto_checkert::resultt::progresst::DONE)
     {
       // loop until we are done
+      ++iterations;
     }
     return determine_result(properties);
   }
 
   void report() override
   {
-    output_properties(properties, ui_message_handler);
+    output_properties(properties, iterations, ui_message_handler);
     output_overall_result(determine_result(properties), ui_message_handler);
   }
 
 protected:
   abstract_goto_modelt &goto_model;
   incremental_goto_checkerT incremental_goto_checker;
+  std::size_t iterations = 1;
 };
 
 #endif // CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_H