Single-path symex checker [blocks: #3976]

jbmc/src/java_bytecode/java_single_path_symex_checker.h

@@ -0,0 +1,37 @@
+/*******************************************************************\
+
+Module: Goto Checker using Single Path Symbolic Execution for Java
+
+Author: Daniel Kroening, Peter Schrammel
+
+ \*******************************************************************/
+
+/// \file
+/// Goto Checker using Single Path Symbolic Execution for Java
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_CHECKER_H
+#define CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_CHECKER_H
+
+#include <goto-checker/single_path_symex_checker.h>
+
+#include "java_bmc_util.h"
+
+class java_single_path_symex_checkert : public single_path_symex_checkert
+{
+public:
+  java_single_path_symex_checkert(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler,
+    abstract_goto_modelt &goto_model)
+    : single_path_symex_checkert(options, ui_message_handler, goto_model)
+  {
+  }
+
+  void setup_symex(symex_bmct &symex) override
+  {
+    single_path_symex_checkert::setup_symex(symex);
+    java_setup_symex(options, goto_model, symex);
+  }
+};
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_CHECKER_H

jbmc/src/java_bytecode/java_single_path_symex_only_checker.h

@@ -0,0 +1,38 @@
+/*******************************************************************\
+
+Module: Goto Checker using Single Path Symbolic Execution for Java
+
+Author: Daniel Kroening, Peter Schrammel
+
+ \*******************************************************************/
+
+/// \file
+/// Goto Checker using Single Path Symbolic Execution for Java
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
+#define CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
+
+#include <goto-checker/single_path_symex_only_checker.h>
+
+#include "java_bmc_util.h"
+
+class java_single_path_symex_only_checkert
+  : public single_path_symex_only_checkert
+{
+public:
+  java_single_path_symex_only_checkert(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler,
+    abstract_goto_modelt &goto_model)
+    : single_path_symex_only_checkert(options, ui_message_handler, goto_model)
+  {
+  }
+
+  void setup_symex(symex_bmct &symex) override
+  {
+    single_path_symex_only_checkert::setup_symex(symex);
+    java_setup_symex(options, goto_model, symex);
+  }
+};
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -66,6 +66,8 @@ Author: Daniel Kroening, [email protected]
 #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/java_single_path_symex_checker.h>
+#include <java_bytecode/java_single_path_symex_only_checker.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/remove_java_new.h>
@@ -559,46 +561,79 @@ int jbmc_parse_optionst::doit()
       options.get_bool_option("program-only") ||
       options.get_bool_option("show-vcc"))
     {
-      if(!options.get_bool_option("paths"))
+      if(options.get_bool_option("paths"))
+      {
+        all_properties_verifiert<java_single_path_symex_only_checkert> verifier(
+          options, ui_message_handler, goto_model);
+        (void)verifier();
+      }
+      else
       {
         all_properties_verifiert<java_multi_path_symex_only_checkert> verifier(
           options, ui_message_handler, goto_model);
         (void)verifier();
-        return CPROVER_EXIT_SUCCESS;
       }
+
+      return CPROVER_EXIT_SUCCESS;
     }
 
     if(
       options.get_bool_option("dimacs") ||
       !options.get_option("outfile").empty())
     {
-      if(!options.get_bool_option("paths"))
+      if(options.get_bool_option("paths"))
+      {
+        stop_on_fail_verifiert<java_single_path_symex_checkert> verifier(
+          options, ui_message_handler, goto_model);
+        (void)verifier();
+      }
+      else
       {
-        stop_on_fail_verifiert<multi_path_symex_checkert> verifier(
+        stop_on_fail_verifiert<java_multi_path_symex_checkert> verifier(
           options, ui_message_handler, goto_model);
         (void)verifier();
-        return CPROVER_EXIT_SUCCESS;
       }
+
+      return CPROVER_EXIT_SUCCESS;
     }
 
     std::unique_ptr<goto_verifiert> verifier = nullptr;
 
     if(
-      !options.get_bool_option("paths") && !options.is_set("cover") &&
-      !options.get_bool_option("dimacs") &&
+      !options.is_set("cover") && !options.get_bool_option("dimacs") &&
       options.get_option("outfile").empty())
     {
       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);
+        if(options.get_bool_option("paths"))
+        {
+          verifier = util_make_unique<
+            stop_on_fail_verifiert<java_single_path_symex_checkert>>(
+            options, ui_message_handler, goto_model);
+        }
+        else
+        {
+          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>>(
-          options, ui_message_handler, goto_model);
+        if(options.get_bool_option("paths"))
+        {
+          verifier =
+            util_make_unique<all_properties_verifier_with_trace_storaget<
+              java_single_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>>(
+              options, ui_message_handler, goto_model);
+        }
       }
     }
 

src/cbmc/cbmc_parse_options.cpp

@@ -40,6 +40,8 @@ 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/single_path_symex_checker.h>
+#include <goto-checker/single_path_symex_only_checker.h>
 #include <goto-checker/stop_on_fail_verifier.h>
 
 #include <goto-programs/adjust_float_expressions.h>
@@ -559,25 +561,39 @@ int cbmc_parse_optionst::doit()
     options.get_bool_option("program-only") ||
     options.get_bool_option("show-vcc"))
   {
-    if(!options.get_bool_option("paths"))
+    if(options.get_bool_option("paths"))
+    {
+      all_properties_verifiert<single_path_symex_only_checkert> verifier(
+        options, ui_message_handler, goto_model);
+      (void)verifier();
+    }
+    else
     {
       all_properties_verifiert<multi_path_symex_only_checkert> verifier(
         options, ui_message_handler, goto_model);
       (void)verifier();
-      return CPROVER_EXIT_SUCCESS;
     }
+
+    return CPROVER_EXIT_SUCCESS;
   }
 
   if(
     options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
   {
-    if(!options.get_bool_option("paths"))
+    if(options.get_bool_option("paths"))
+    {
+      stop_on_fail_verifiert<single_path_symex_checkert> verifier(
+        options, ui_message_handler, goto_model);
+      (void)verifier();
+    }
+    else
     {
       stop_on_fail_verifiert<multi_path_symex_checkert> verifier(
         options, ui_message_handler, goto_model);
       (void)verifier();
-      return CPROVER_EXIT_SUCCESS;
     }
+
+    return CPROVER_EXIT_SUCCESS;
   }
 
   if(options.is_set("cover"))
@@ -596,20 +612,36 @@ int cbmc_parse_optionst::doit()
   std::unique_ptr<goto_verifiert> verifier = nullptr;
 
   if(
-    !options.get_bool_option("paths") && !options.is_set("cover") &&
-    !options.get_bool_option("dimacs") && options.get_option("outfile").empty())
+    !options.is_set("cover") && !options.get_bool_option("dimacs") &&
+    options.get_option("outfile").empty())
   {
     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);
+      if(options.get_bool_option("paths"))
+      {
+        verifier =
+          util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
+            options, ui_message_handler, goto_model);
+      }
+      else
+      {
+        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>>(
-        options, ui_message_handler, goto_model);
+      if(options.get_bool_option("paths"))
+      {
+        verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
+          single_path_symex_checkert>>(options, ui_message_handler, goto_model);
+      }
+      else
+      {
+        verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
+          multi_path_symex_checkert>>(options, ui_message_handler, goto_model);
+      }
     }
   }
 

src/goto-checker/Makefile

@@ -2,12 +2,15 @@ SRC = bmc_util.cpp \
       counterexample_beautification.cpp \
       cover_goals_report_util.cpp \
       incremental_goto_checker.cpp \
+      goto_symex_property_decider.cpp \
       goto_trace_storage.cpp \
       goto_verifier.cpp \
       multi_path_symex_checker.cpp \
       multi_path_symex_only_checker.cpp \
       properties.cpp \
       report_util.cpp \
+      single_path_symex_checker.cpp \
+      single_path_symex_only_checker.cpp \
       solver_factory.cpp \
       symex_coverage.cpp \
       symex_bmc.cpp \

src/goto-checker/bmc_util.cpp

@@ -269,3 +269,104 @@ void update_status_of_not_checked_properties(
     }
   }
 }
+
+void update_status_of_unknown_properties(
+  propertiest &properties,
+  std::unordered_set<irep_idt> &updated_properties)
+{
+  for(auto &property_pair : properties)
+  {
+    if(property_pair.second.status == property_statust::UNKNOWN)
+    {
+      // This could have any status except NOT_CHECKED.
+      // We consider them PASS because we do verification modulo bounds.
+      property_pair.second.status = property_statust::PASS;
+      updated_properties.insert(property_pair.first);
+    }
+  }
+}
+
+void output_coverage_report(
+  const std::string &cov_out,
+  const abstract_goto_modelt &goto_model,
+  const symex_bmct &symex,
+  ui_message_handlert &ui_message_handler)
+{
+  if(
+    !cov_out.empty() &&
+    symex.output_coverage_report(goto_model.get_goto_functions(), cov_out))
+  {
+    messaget log(ui_message_handler);
+    log.error() << "Failed to write symex coverage report to '" << cov_out
+                << "'" << messaget::eom;
+  }
+}
+
+static void postprocess_equation(
+  symex_bmct &symex,
+  symex_target_equationt &equation,
+  const optionst &options,
+  const namespacet &ns,
+  ui_message_handlert &ui_message_handler)
+{
+  // add a partial ordering, if required
+  if(equation.has_threads())
+  {
+    std::unique_ptr<memory_model_baset> memory_model =
+      get_memory_model(options, ns);
+    memory_model->set_message_handler(ui_message_handler);
+    (*memory_model)(equation);
+  }
+
+  messaget log(ui_message_handler);
+  log.statistics() << "size of program expression: "
+                   << equation.SSA_steps.size() << " steps" << messaget::eom;
+
+  slice(symex, equation, ns, options, ui_message_handler);
+
+  if(options.get_bool_option("validate-ssa-equation"))
+  {
+    symex.validate(validation_modet::INVARIANT);
+  }
+}
+
+void perform_symex(
+  abstract_goto_modelt &goto_model,
+  symex_bmct &symex,
+  symbol_tablet &symex_symbol_table,
+  symex_target_equationt &equation,
+  const optionst &options,
+  const namespacet &ns,
+  ui_message_handlert &ui_message_handler)
+{
+  auto get_goto_function =
+    [&goto_model](
+      const irep_idt &id) -> const goto_functionst::goto_functiont & {
+    return goto_model.get_goto_function(id);
+  };
+
+  symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
+
+  postprocess_equation(symex, equation, options, ns, ui_message_handler);
+}
+
+void perform_symex(
+  abstract_goto_modelt &goto_model,
+  symex_bmct &symex,
+  path_storaget::patht &resume,
+  symbol_tablet &symex_symbol_table,
+  const optionst &options,
+  const namespacet &ns,
+  ui_message_handlert &ui_message_handler)
+{
+  auto get_goto_function =
+    [&goto_model](
+      const irep_idt &id) -> const goto_functionst::goto_functiont & {
+    return goto_model.get_goto_function(id);
+  };
+
+  symex.resume_symex_from_saved_state(
+    get_goto_function, resume.state, &resume.equation, symex_symbol_table);
+
+  postprocess_equation(symex, resume.equation, options, ns, ui_message_handler);
+}