Proposal: introduce a goto-checker module [blocks: #2212, #3268]

CMakeLists.txt

@@ -58,6 +58,7 @@ set_target_properties(
     goto-analyzer-lib
     goto-cc
     goto-cc-lib
+    goto-checker
     goto-diff
     goto-diff-lib
     goto-instrument

jbmc/src/jbmc/CMakeLists.txt

@@ -12,6 +12,7 @@ target_link_libraries(jbmc-lib
     ansi-c
     big-int
     cbmc-lib
+    goto-checker
     goto-instrument-lib
     goto-programs
     goto-symex

jbmc/src/jbmc/Makefile

@@ -6,6 +6,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../java_bytecode/java_bytecode$(LIBEXT) \
       ../$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
       ../$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-symex/goto-symex$(LIBEXT) \
       ../$(CPROVER_DIR)/src/pointer-analysis/value_set$(OBJEXT) \

src/CMakeLists.txt

@@ -85,6 +85,7 @@ add_subdirectory(ansi-c)
 add_subdirectory(assembler)
 add_subdirectory(big-int)
 add_subdirectory(cpp)
+add_subdirectory(goto-checker)
 add_subdirectory(goto-programs)
 add_subdirectory(goto-symex)
 add_subdirectory(jsil)

src/Makefile

@@ -6,6 +6,7 @@ DIRS = analyses \
        cpp \
        goto-analyzer \
        goto-cc \
+       goto-checker \
        goto-diff \
        goto-instrument \
        goto-programs \
@@ -49,9 +50,11 @@ goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
                      goto-symex.dir linking.dir analyses.dir solvers.dir \
                      json.dir
 
+goto-checker.dir: solvers.dir goto-symex.dir goto-programs.dir
+
 cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
           pointer-analysis.dir goto-programs.dir linking.dir \
-          goto-instrument.dir
+          goto-instrument.dir goto-checker.dir
 
 goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
                    json.dir goto-instrument.dir

src/cbmc/Makefile

@@ -16,6 +16,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
+      ../goto-checker/goto-checker$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \
       ../goto-symex/goto-symex$(LIBEXT) \
       ../pointer-analysis/value_set$(OBJEXT) \

src/goto-checker/CMakeLists.txt

@@ -0,0 +1,6 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(goto-checker ${sources})
+
+generic_includes(goto-checker)
+
+target_link_libraries(goto-checker goto-programs goto-symex solvers util)

src/goto-checker/Makefile

@@ -0,0 +1,17 @@
+SRC = property_checker.cpp \
+      safety_checker.cpp \
+      # Empty last line
+
+INCLUDES= -I ..
+
+include ../config.inc
+include ../common
+
+CLEANFILES = goto-checker$(LIBEXT)
+
+all: goto-checker$(LIBEXT)
+
+###############################################################################
+
+goto-checker$(LIBEXT): $(OBJ)
+	$(LINKLIB)

src/goto-checker/goto_checker.cpp

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Goto Checker Interface
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto Checker Interface
+
+#include "goto_checker.h"
+
+goto_checkert::goto_checkert(
+  const optionst &options,
+  ui_message_handlert &ui_message_handler)
+  : messaget(ui_message_handler),
+    options(options),
+    ui_message_handler(ui_message_handler)
+{
+}

src/goto-checker/goto_checker.h

@@ -0,0 +1,56 @@
+/*******************************************************************\
+
+Module: Goto Checker Interface
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto Checker Interface
+
+#ifndef CPROVER_GOTO_CHECKER_GOTO_CHECKER_H
+#define CPROVER_GOTO_CHECKER_GOTO_CHECKER_H
+
+#include <goto-programs/goto_trace.h>
+
+#include <util/options.h>
+#include <util/ui_message.h>
+
+#include "properties.h"
+
+/// An implementation of `goto_checkert` provides functionality for
+/// checking a set of properties and returning counterexamples
+/// one by one to the caller.
+/// An implementation of `goto_checkert` is responsible for maintaining
+/// the state of the analysis that it performs (e.g. goto-symex, solver, etc).
+/// It is not responsible for maintaining outcomes (e.g. property results,
+/// counterexamples, etc). However, an implementation may restrict the
+/// sets of properties it is asked to check (e.g. only sequences of subsets).
+class goto_checkert : public messaget
+{
+public:
+  /// Check whether the given properties with status UNKNOWN or newly
+  /// discovered properties hold
+  /// \return The properties whose status has been determined
+  /// If there is a property with status FAIL then its counterexample
+  /// can be retrieved by calling `build_error_trace` before any
+  /// subsequent call to operator().
+  /// `goto_checkert` derivatives shall be implemented in a way such
+  /// that repeated calls to operator() shall return the next FAILed
+  /// property until eventually not returning any FAILing properties.
+  virtual propertiest operator()(const propertiest &) = 0;
+
+  /// This builds and returns the counterexample
+  virtual goto_tracet build_error_trace() = 0;
+
+protected:
+  goto_checkert(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler);
+
+  const optionst &options;
+  ui_message_handlert &ui_message_handler;
+};
+
+#endif // CPROVER_GOTO_CHECKER_GOTO_CHECKER_H

src/goto-checker/goto_verifier.cpp

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Goto Verifier Interface
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto Verifier Interface
+
+#include "goto_verifier.h"
+
+goto_verifiert::goto_verifiert(
+  const optionst &_options,
+  ui_message_handlert &ui_message_handler)
+  : messaget(ui_message_handler),
+    options(_options),
+    ui_message_handler(ui_message_handler)
+{
+}

src/goto-checker/goto_verifier.h

@@ -0,0 +1,55 @@
+/*******************************************************************\
+
+Module: Goto Verifier Interface
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto Verifier Interface
+
+#ifndef CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H
+#define CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H
+
+#include <util/optional.h>
+#include <util/options.h>
+#include <util/ui_message.h>
+
+#include "properties.h"
+
+/// An implementation of `goto_verifiert` checks all properties in
+/// a goto model. It typically uses, but doesn't have to use, a
+/// `goto_checkert` to iteratively determine the verification result
+/// of each property.
+class goto_verifiert : public messaget
+{
+public:
+  /// Check whether all properties hold.
+  /// \return PASS if all properties are PASS,
+  ///         FAIL if at least one property is FAIL and no property is ERROR,
+  ///         UNKNOWN if no property is FAIL or ERROR and
+  ///           at least one property is UNKNOWN,
+  ///         ERROR if at least one property is error.
+  virtual resultt operator()() = 0;
+
+  /// Report results
+  virtual void report() = 0;
+
+  /// Returns the properties
+  const propertiest &get_properties()
+  {
+    return properties;
+  }
+
+protected:
+  goto_verifiert(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler);
+
+  const optionst &options;
+  ui_message_handlert &ui_message_handler;
+  propertiest properties;
+};
+
+#endif // CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H

src/goto-checker/properties.cpp

@@ -0,0 +1,138 @@
+/*******************************************************************\
+
+Module: Goto Checker Interface
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Property Map
+
+#include "properties.h"
+
+#include <util/invariant.h>
+
+std::string as_string(resultt result)
+{
+  switch(result)
+  {
+  case resultt::PASS:
+    return "PASS";
+  case resultt::FAIL:
+    return "FAIL";
+  case resultt::ERROR:
+    return "ERROR";
+  case resultt::UNKNOWN:
+    return "UNKNOWN";
+  }
+
+  UNREACHABLE;
+}
+
+/// Returns the properties in the goto model
+propertiest initialize_properties(const goto_modelt &goto_model)
+{
+  propertiest properties;
+  forall_goto_functions(it, goto_model.goto_functions)
+  {
+    if(
+      !it->second.is_inlined() ||
+      it->first == goto_model.goto_functions.entry_point())
+    {
+      const goto_programt &goto_program = it->second.body;
+
+      forall_goto_program_instructions(i_it, goto_program)
+      {
+        if(!i_it->is_assert())
+          continue;
+
+        const source_locationt &source_location = i_it->source_location;
+
+        irep_idt property_id = source_location.get_property_id();
+
+        property_infot &property = properties[property_id];
+        property.result = resultt::UNKNOWN;
+        property.location = i_it;
+      }
+    }
+  }
+  return properties;
+}
+
+/// Update with the preference order
+/// 1. old non-UNKNOWN result
+/// 2. new non-UNKNOWN result
+/// 3. UNKNOWN
+/// Suitable for updating property results
+resultt &operator|=(resultt &a, resultt const &b)
+{
+  PRECONDITION(a == resultt::UNKNOWN || a == b);
+  switch(a)
+  {
+  case resultt::UNKNOWN:
+    a = b;
+    return a;
+  case resultt::ERROR:
+  case resultt::PASS:
+  case resultt::FAIL:
+    return a;
+  }
+  UNREACHABLE;
+}
+
+/// Update with the preference order
+/// 1. ERROR
+/// 2. FAIL
+/// 3. UNKNOWN
+/// 4. PASS
+/// Suitable for computing overall results
+resultt &operator&=(resultt &a, resultt const &b)
+{
+  switch(a)
+  {
+  case resultt::UNKNOWN:
+    a = b;
+    return a;
+  case resultt::PASS:
+    a = (b == resultt::PASS ? a : b);
+    return a;
+  case resultt::ERROR:
+    a = b;
+    return a;
+  case resultt::FAIL:
+    a = (b == resultt::ERROR ? b : a);
+    return a;
+  }
+  UNREACHABLE;
+}
+
+/// Determines the overall result corresponding from the given properties
+/// That is PASS if all properties are PASS,
+///         FAIL if at least one property is FAIL and no property is ERROR,
+///         UNKNOWN if no property is FAIL or ERROR and
+///           at least one property is UNKNOWN,
+///         ERROR if at least one property is error.
+resultt determine_result(const propertiest &properties)
+{
+  resultt result = resultt::UNKNOWN;
+  for(const auto &property_pair : properties)
+  {
+    result &= property_pair.second.result;
+  }
+  return result;
+}
+
+/// Merges a set of properties into a given set of properties,
+/// updating its results and adding new properties.
+void merge_properties(
+  propertiest &properties,
+  const propertiest &updated_properties)
+{
+  for(const auto &property_pair : updated_properties)
+  {
+    auto found_property = properties.insert(property_pair);
+    if(!found_property.second)
+      found_property.first->second.result |= property_pair.second.result;
+  }
+}