From fd258c3515ea40e87b56705c9b35a9bb86547a23 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Tue, 9 Jul 2019 17:46:00 +0200 Subject: [PATCH] improve verification of crashing programs --- src/mc/ModelChecker.cpp | 8 ++- teshsuite/mc/CMakeLists.txt | 21 ++++++-- .../mc/random-bug/random-bug-replay.tesh | 12 +++++ .../mc/random-bug/random-bug-report.tesh | 14 ------ teshsuite/mc/random-bug/random-bug.c | 37 -------------- teshsuite/mc/random-bug/random-bug.cpp | 49 +++++++++++++++++++ teshsuite/mc/random-bug/random-bug.tesh | 43 +++++++++++++++- 7 files changed, 125 insertions(+), 59 deletions(-) create mode 100644 teshsuite/mc/random-bug/random-bug-replay.tesh delete mode 100644 teshsuite/mc/random-bug/random-bug-report.tesh delete mode 100644 teshsuite/mc/random-bug/random-bug.c create mode 100644 teshsuite/mc/random-bug/random-bug.cpp diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 4250bffe34..3cf073e973 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -150,8 +150,12 @@ static void MC_report_crash(int status) XBT_INFO(" %s", s.c_str()); simgrid::mc::dumpRecordPath(); simgrid::mc::session->log_state(); - XBT_INFO("Stack trace:"); - mc_model_checker->process().dump_stack(); + if (xbt_log_no_loc) { + XBT_INFO("Stack trace not displayed because you passed --log=no_loc"); + } else { + XBT_INFO("Stack trace:"); + mc_model_checker->process().dump_stack(); + } } static void MC_report_assertion_error() diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt index 85fc94b2d0..86820cdcaa 100644 --- a/teshsuite/mc/CMakeLists.txt +++ b/teshsuite/mc/CMakeLists.txt @@ -1,3 +1,4 @@ +# MC-only C++ binaries foreach(x dwarf dwarf-expression) if (SIMGRID_HAVE_MC) add_executable (${x} EXCLUDE_FROM_ALL ${x}/${x}.cpp) @@ -11,13 +12,25 @@ foreach(x dwarf dwarf-expression) set(teshsuite_src ${teshsuite_src} ${CMAKE_CURRENT_SOURCE_DIR}/${x}/${x}.cpp) endforeach() +# MC-independent C++ binaries +foreach(x random-bug) + add_executable (${x} EXCLUDE_FROM_ALL ${x}/${x}.cpp) + target_link_libraries(${x} simgrid) + set_target_properties(${x} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${x}) + set_property(TARGET ${x} APPEND PROPERTY INCLUDE_DIRECTORIES "${INTERNAL_INCLUDES}") + add_dependencies(tests ${x}) + + set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${x}/${x}.tesh) + set(teshsuite_src ${teshsuite_src} ${CMAKE_CURRENT_SOURCE_DIR}/${x}/${x}.cpp) +endforeach() + add_executable (without-mutex-handling EXCLUDE_FROM_ALL mutex-handling/mutex-handling.c) target_link_libraries(without-mutex-handling simgrid) set_target_properties(without-mutex-handling PROPERTIES COMPILE_FLAGS -DDISABLE_THE_MUTEX=1) set_target_properties(without-mutex-handling PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/mutex-handling) add_dependencies(tests without-mutex-handling) -foreach(x mutex-handling random-bug) +foreach(x mutex-handling) add_executable (${x} EXCLUDE_FROM_ALL ${x}/${x}.c) target_link_libraries(${x} simgrid) set_target_properties(${x} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${x}) @@ -28,7 +41,7 @@ foreach(x mutex-handling random-bug) endforeach() set(teshsuite_src ${teshsuite_src} PARENT_SCOPE) -set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/random-bug/random-bug-report.tesh +set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/random-bug/random-bug-replay.tesh ${CMAKE_CURRENT_SOURCE_DIR}/mutex-handling/without-mutex-handling.tesh PARENT_SCOPE) set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/mutex-handling/mutex-handling_d.xml PARENT_SCOPE) @@ -39,7 +52,7 @@ IF(SIMGRID_HAVE_MC) # ADD_TESH(tesh-mc-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling mutex-handling.tesh --cfg=model-check/reduction:dpor) ADD_TESH(tesh-mc-without-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:none) ADD_TESH(tesh-mc-without-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:dpor) - ADD_TESH(mc-random-bug-record --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug-report.tesh) + ADD_TESH(mc-random-bug --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug.tesh) ENDIF() -ADD_TESH(mc-random-bug --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug.tesh) +ADD_TESH(mc-random-bug-replay --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug-replay.tesh) diff --git a/teshsuite/mc/random-bug/random-bug-replay.tesh b/teshsuite/mc/random-bug/random-bug-replay.tesh new file mode 100644 index 0000000000..f49f474f6f --- /dev/null +++ b/teshsuite/mc/random-bug/random-bug-replay.tesh @@ -0,0 +1,12 @@ +#!/usr/bin/env tesh +$ ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" "--cfg=model-check/replay:1/3;1/4" +> Behavior: printf +> [ 0.000000] (0:maestro@) path=1/3;1/4 +> Error reached + +# Behavior: assert does not have the same output within and without MC, so don't test it here. That's already covered with the other ones + +! expect signal SIGIOT +$ ${bindir:=.}/random-bug abort ${platfdir}/small_platform.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" "--cfg=model-check/replay:1/3;1/4" +> Behavior: abort +> [ 0.000000] (0:maestro@) path=1/3;1/4 diff --git a/teshsuite/mc/random-bug/random-bug-report.tesh b/teshsuite/mc/random-bug/random-bug-report.tesh deleted file mode 100644 index 2cf11154cd..0000000000 --- a/teshsuite/mc/random-bug/random-bug-report.tesh +++ /dev/null @@ -1,14 +0,0 @@ -#!/usr/bin/env tesh -! expect return 1 -$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug ${srcdir:=.}/examples/platforms/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning -> [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor. -> [ 0.000000] (0:maestro@) ************************** -> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID *** -> [ 0.000000] (0:maestro@) ************************** -> [ 0.000000] (0:maestro@) Counter-example execution trace: -> [ 0.000000] (0:maestro@) [(1)Tremblay (app)] MC_RANDOM(3) -> [ 0.000000] (0:maestro@) [(1)Tremblay (app)] MC_RANDOM(4) -> [ 0.000000] (0:maestro@) Path = 1/3;1/4 -> [ 0.000000] (0:maestro@) Expanded states = 27 -> [ 0.000000] (0:maestro@) Visited states = 68 -> [ 0.000000] (0:maestro@) Executed transitions = 46 diff --git a/teshsuite/mc/random-bug/random-bug.c b/teshsuite/mc/random-bug/random-bug.c deleted file mode 100644 index 825392df36..0000000000 --- a/teshsuite/mc/random-bug/random-bug.c +++ /dev/null @@ -1,37 +0,0 @@ -/* Copyright (c) 2014-2019. The SimGrid Team. All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - -#include -#include - -#include /* snprintf */ - -XBT_LOG_NEW_DEFAULT_CATEGORY(random_bug, "Application"); - -/** An (fake) application with a bug occuring for some random values */ -static int app(XBT_ATTRIB_UNUSED int argc, XBT_ATTRIB_UNUSED char* argv[]) -{ - int x = MC_random(0, 5); - int y = MC_random(0, 5); - - if (MC_is_active()) { - MC_assert(x !=3 || y !=4); - } - if (x ==3 && y ==4) { - fprintf(stderr, "Error reached\n"); - } - - return 0; -} - -/** Main function */ -int main(int argc, char *argv[]) -{ - MSG_init(&argc, argv); - MSG_function_register("app", &app); - MSG_create_environment(argv[1]); - MSG_process_create("app", app, NULL, MSG_get_host_by_name("Tremblay")); - return MSG_main(); -} diff --git a/teshsuite/mc/random-bug/random-bug.cpp b/teshsuite/mc/random-bug/random-bug.cpp new file mode 100644 index 0000000000..4f3a9f88b3 --- /dev/null +++ b/teshsuite/mc/random-bug/random-bug.cpp @@ -0,0 +1,49 @@ +/* Copyright (c) 2014-2019. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include +#include + +#include /* snprintf */ + +enum { ABORT, ASSERT, PRINTF } behavior; + +/** An (fake) application with a bug occuring for some random values */ +static void app() +{ + int x = MC_random(0, 5); + int y = MC_random(0, 5); + + if (behavior == ABORT) { + abort(); + } else if (behavior == ASSERT) { + MC_assert(x != 3 || y != 4); + } else if (behavior == PRINTF) { + if (x == 3 && y == 4) + fprintf(stderr, "Error reached\n"); + } +} + +/** Main function */ +int main(int argc, char* argv[]) +{ + simgrid::s4u::Engine e(&argc, argv); + xbt_assert(argc == 3, "Usage: random-bug raise|assert "); + if (strcmp(argv[1], "abort") == 0) { + printf("Behavior: abort\n"); + behavior = ABORT; + } else if (strcmp(argv[1], "assert") == 0) { + printf("Behavior: assert\n"); + behavior = ASSERT; + } else if (strcmp(argv[1], "printf") == 0) { + printf("Behavior: printf\n"); + behavior = PRINTF; + } + + e.load_platform(argv[2]); + + simgrid::s4u::Actor::create("app", simgrid::s4u::Host::by_name("Fafard"), &app); + e.run(); +} diff --git a/teshsuite/mc/random-bug/random-bug.tesh b/teshsuite/mc/random-bug/random-bug.tesh index c3f29d95ed..8e097de364 100644 --- a/teshsuite/mc/random-bug/random-bug.tesh +++ b/teshsuite/mc/random-bug/random-bug.tesh @@ -1,4 +1,43 @@ #!/usr/bin/env tesh -$ ${bindir:=.}/random-bug ${srcdir:=.}/examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" "--cfg=model-check/replay:1/3;1/4" -> [ 0.000000] (0:maestro@) path=1/3;1/4 +! expect return 1 +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning +> [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor. +> Behavior: assert +> [ 0.000000] (0:maestro@) ************************** +> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID *** +> [ 0.000000] (0:maestro@) ************************** +> [ 0.000000] (0:maestro@) Counter-example execution trace: +> [ 0.000000] (0:maestro@) [(1)Fafard (app)] MC_RANDOM(3) +> [ 0.000000] (0:maestro@) [(1)Fafard (app)] MC_RANDOM(4) +> [ 0.000000] (0:maestro@) Path = 1/3;1/4 +> [ 0.000000] (0:maestro@) Expanded states = 27 +> [ 0.000000] (0:maestro@) Visited states = 68 +> [ 0.000000] (0:maestro@) Executed transitions = 46 + +! expect return 6 +# because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6 +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug abort ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --log=no_loc +> [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor. +> Behavior: abort +> [ 0.000000] (0:maestro@) ************************** +> [ 0.000000] (0:maestro@) ** CRASH IN THE PROGRAM ** +> [ 0.000000] (0:maestro@) ************************** +> [ 0.000000] (0:maestro@) From signal: Aborted +> [ 0.000000] (0:maestro@) No core dump was generated by the system. +> [ 0.000000] (0:maestro@) Counter-example execution trace: +> [ 0.000000] (0:maestro@) [(1)Fafard (app)] MC_RANDOM(0) +> [ 0.000000] (0:maestro@) [(1)Fafard (app)] MC_RANDOM(0) +> [ 0.000000] (0:maestro@) Path = 1;1 +> [ 0.000000] (0:maestro@) Expanded states = 2 +> [ 0.000000] (0:maestro@) Visited states = 2 +> [ 0.000000] (0:maestro@) Executed transitions = 2 +> [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc + +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning +> [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor. +> Behavior: printf > Error reached +> [ 0.000000] (0:maestro@) No property violation found. +> [ 0.000000] (0:maestro@) Expanded states = 43 +> [ 0.000000] (0:maestro@) Visited states = 108 +> [ 0.000000] (0:maestro@) Executed transitions = 72 -- 2.20.1