Multi-path symex-only checker [blocks: 3795]

jbmc/src/java_bytecode/Makefile

@@ -7,6 +7,7 @@ SRC = bytecode_info.cpp \
       generic_parameter_specialization_map_keys.cpp \
       jar_file.cpp \
       jar_pool.cpp \
+      java_bmc_util.cpp \
       java_bytecode_convert_class.cpp \
       java_bytecode_convert_method.cpp \
       java_bytecode_concurrency_instrumentation.cpp \

jbmc/src/java_bytecode/java_bmc_util.cpp

@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+Module: Bounded Model Checking Utils for Java
+
+Author: Daniel Kroening, Peter Schrammel
+
+ \*******************************************************************/
+
+/// \file
+/// Bounded Model Checking Utils for Java
+
+#include "java_bmc_util.h"
+
+#include <goto-checker/symex_bmc.h>
+#include <goto-programs/abstract_goto_model.h>
+#include <java_bytecode/java_enum_static_init_unwind_handler.h>
+
+void java_setup_symex(
+  const optionst &options,
+  abstract_goto_modelt &goto_model,
+  symex_bmct &symex)
+{
+  // unwinds <clinit> loops to number of enum elements
+  if(options.get_bool_option("java-unwind-enum-static"))
+  {
+    // clang-format off
+    // (it asks for the body to be at the same indent level as the parameters
+    //  for some reason)
+    symex.add_loop_unwind_handler(
+      [&goto_model](
+        const goto_symex_statet::call_stackt &context,
+        unsigned loop_num,
+        unsigned unwind,
+        unsigned &max_unwind)
+      { // NOLINT (*)
+        return java_enum_static_init_unwind_handler(
+          context, loop_num, unwind, max_unwind, goto_model.get_symbol_table());
+      });
+    // clang-format on
+  }
+}

jbmc/src/java_bytecode/java_bmc_util.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Bounded Model Checking Utils for Java
+
+Author: Daniel Kroening, Peter Schrammel
+
+ \*******************************************************************/
+
+/// \file
+/// Bounded Model Checking Utils for Java
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H
+#define CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H
+
+class abstract_goto_modelt;
+class optionst;
+class symex_bmct;
+
+/// Registers Java-specific preprocessing handlers with goto-symex
+void java_setup_symex(
+  const optionst &options,
+  abstract_goto_modelt &goto_model,
+  symex_bmct &symex);
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H

jbmc/src/java_bytecode/java_multi_path_symex_only_checker.h

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+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_ONLY_CHECKER_H
+#define CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_ONLY_CHECKER_H
+
+#include <goto-checker/multi_path_symex_only_checker.h>
+
+#include "java_bmc_util.h"
+
+class java_multi_path_symex_only_checkert
+  : public multi_path_symex_only_checkert
+{
+public:
+  java_multi_path_symex_only_checkert(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler,
+    abstract_goto_modelt &goto_model)
+    : multi_path_symex_only_checkert(options, ui_message_handler, goto_model)
+  {
+    java_setup_symex(options, goto_model, symex);
+  }
+};
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_ONLY_CHECKER_H

jbmc/src/java_bytecode/module_dependencies.txt

@@ -1,5 +1,6 @@
 analyses
 ansi-c # should go away
+goto-checker
 goto-programs
 java_bytecode
 json

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -27,6 +27,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/ansi_c_language.h>
 
+#include <goto-checker/all_properties_verifier.h>
+
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
@@ -60,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_only_checker.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/remove_java_new.h>
@@ -563,6 +566,19 @@ int jbmc_parse_optionst::doit()
       goto_model.validate(validation_modet::INVARIANT);
     }
 
+    if(
+      options.get_bool_option("program-only") ||
+      options.get_bool_option("show-vcc"))
+    {
+      if(!options.get_bool_option("paths"))
+      {
+        all_properties_verifiert<java_multi_path_symex_only_checkert> verifier(
+          options, ui_message_handler, goto_model);
+        (void)verifier();
+        return CPROVER_EXIT_SUCCESS;
+      }
+    }
+
     // The `configure_bmc` callback passed will enable enum-unwind-static if
     // applicable.
     return bmct::do_language_agnostic_bmc(

src/cbmc/cbmc_parse_options.cpp

@@ -30,7 +30,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <cpp/cprover_library.h>
 
+#include <goto-checker/all_properties_verifier.h>
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/multi_path_symex_only_checker.h>
+#include <goto-checker/properties.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
@@ -553,6 +556,19 @@ int cbmc_parse_optionst::doit()
     goto_model.validate(validation_modet::INVARIANT);
   }
 
+  if(
+    options.get_bool_option("program-only") ||
+    options.get_bool_option("show-vcc"))
+  {
+    if(!options.get_bool_option("paths"))
+    {
+      all_properties_verifiert<multi_path_symex_only_checkert> verifier(
+        options, ui_message_handler, goto_model);
+      (void)verifier();
+      return CPROVER_EXIT_SUCCESS;
+    }
+  }
+
   return bmct::do_language_agnostic_bmc(
     options, goto_model, ui_message_handler);
 }

src/goto-checker/Makefile

@@ -1,6 +1,7 @@
 SRC = bmc_util.cpp \
       incremental_goto_checker.cpp \
       goto_verifier.cpp \
+      multi_path_symex_only_checker.cpp \
       properties.cpp \
       report_util.cpp \
       solver_factory.cpp \

src/goto-checker/bmc_util.cpp

@@ -225,3 +225,53 @@ void slice(
                    << " remaining after simplification" << messaget::eom;
 }
 
+std::vector<irep_idt> update_properties_status_from_symex_target_equation(
+  propertiest &properties,
+  const symex_target_equationt &equation)
+{
+  std::vector<irep_idt> updated_properties;
+
+  for(const auto &step : equation.SSA_steps)
+  {
+    if(!step.is_assert())
+      continue;
+
+    irep_idt property_id = step.get_property_id();
+
+    if(property_id.empty())
+      continue;
+
+    // Don't set false properties; we wouldn't have traces for them.
+    const auto status = step.cond_expr.is_true() ? property_statust::PASS
+                                                 : property_statust::UNKNOWN;
+    auto emplace_result = properties.emplace(
+      property_id, property_infot{step.source.pc, step.comment, status});
+
+    if(emplace_result.second)
+    {
+      updated_properties.push_back(property_id);
+    }
+    else
+    {
+      property_infot &property_info = emplace_result.first->second;
+      property_statust old_status = property_info.status;
+      property_info.status |= status;
+
+      if(property_info.status != old_status)
+        updated_properties.push_back(property_id);
+    }
+  }
+
+  for(auto &property_pair : properties)
+  {
+    if(property_pair.second.status == property_statust::NOT_CHECKED)
+    {
+      // This could be a NOT_CHECKED, NOT_REACHABLE or PASS,
+      // but the equation doesn't give us precise information.
+      property_pair.second.status = property_statust::PASS;
+      updated_properties.push_back(property_pair.first);
+    }
+  }
+
+  return updated_properties;
+}

src/goto-checker/bmc_util.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-programs/safety_checker.h>
 
+#include "properties.h"
+
 class goto_tracet;
 class memory_model_baset;
 class message_handlert;
@@ -67,6 +69,13 @@ void slice(
   const optionst &,
   ui_message_handlert &);
 
+/// Sets property status to PASS for properties whose
+/// conditions are constant true.
+/// \return IDs of updated properties
+std::vector<irep_idt> update_properties_status_from_symex_target_equation(
+  propertiest &properties,
+  const symex_target_equationt &equation);
+
 // clang-format off
 #define OPT_BMC \
   "(program-only)" \

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -0,0 +1,98 @@
+/*******************************************************************\
+
+Module: Goto Checker using Multi-Path Symbolic Execution Only
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)
+
+#include "multi_path_symex_only_checker.h"
+
+#include <util/invariant.h>
+
+#include <goto-symex/memory_model_pso.h>
+#include <goto-symex/show_program.h>
+#include <goto-symex/show_vcc.h>
+
+#include "bmc_util.h"
+
+multi_path_symex_only_checkert::multi_path_symex_only_checkert(
+  const optionst &options,
+  ui_message_handlert &ui_message_handler,
+  abstract_goto_modelt &goto_model)
+  : incremental_goto_checkert(options, ui_message_handler),
+    goto_model(goto_model),
+    ns(goto_model.get_symbol_table(), symex_symbol_table),
+    symex(
+      ui_message_handler,
+      goto_model.get_symbol_table(),
+      equation,
+      options,
+      path_storage)
+{
+  setup_symex(symex, ns, options, ui_message_handler);
+}
+
+incremental_goto_checkert::resultt multi_path_symex_only_checkert::
+operator()(propertiest &properties)
+{
+  perform_symex();
+
+  output_coverage_report();
+
+  if(options.get_bool_option("show-vcc"))
+  {
+    show_vcc(options, ui_message_handler, equation);
+  }
+
+  if(options.get_bool_option("program-only"))
+  {
+    show_program(ns, equation);
+  }
+
+  return resultt(
+    resultt::progresst::DONE,
+    update_properties_status_from_symex_target_equation(properties, equation));
+}
+
+void multi_path_symex_only_checkert::perform_symex()
+{
+  auto get_goto_function =
+    [this](const irep_idt &id) -> const goto_functionst::goto_functiont & {
+    return goto_model.get_goto_function(id);
+  };
+
+  // perform symbolic execution
+  symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
+
+  // add a partial ordering, if required
+  // We won't be able to decide any properties by adding this,
+  // but we'd like to see the entire SSA.
+  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);
+  }
+
+  log.statistics() << "size of program expression: "
+                   << equation.SSA_steps.size() << " steps" << messaget::eom;
+
+  slice(symex, equation, ns, options, ui_message_handler);
+}
+
+void multi_path_symex_only_checkert::output_coverage_report()
+{
+  std::string cov_out = options.get_option("symex-coverage-report");
+  if(
+    !cov_out.empty() &&
+    symex.output_coverage_report(goto_model.get_goto_functions(), cov_out))
+  {
+    log.error() << "Failed to write symex coverage report to '" << cov_out
+                << "'" << messaget::eom;
+  }
+}