improve verification of crashing programs

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 4250bff..3cf073e 100644 (file)
--- 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("  %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()
 }
 
 static void MC_report_assertion_error()

diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt
index 85fc94b..86820cd 100644 (file)
--- 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)
 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()
 
   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)
 
 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})
   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)
 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)
 
                                     ${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(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()
 
 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 (file)
index 0000000..f49f474
--- /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 (file)
index 2cf1115..0000000
--- 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 (file)
index 825392d..0000000
--- 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 <simgrid/msg.h>
-#include <simgrid/modelchecker.h>
-
-#include <stdio.h> /* 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 (file)
index 0000000..4f3a9f8
--- /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 <simgrid/modelchecker.h>
+#include <simgrid/s4u.hpp>
+
+#include <stdio.h> /* 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 <platformfile>");
+  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 c3f29d9..8e097de 100644 (file)
--- a/teshsuite/mc/random-bug/random-bug.tesh
+++ b/teshsuite/mc/random-bug/random-bug.tesh
@@ -1,4 +1,43 @@
 #!/usr/bin/env tesh
 #!/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
 > 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