[mc] ptrace the model-checker application

[simgrid.git] / src / mc / mc_server.cpp

diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp
index b882504..e618b32 100644 (file)
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -12,8 +12,11 @@
 #include <sys/wait.h>
 #include <sys/socket.h>
 #include <sys/signalfd.h>
+#include <sys/ptrace.h>
 
 #include <xbt/log.h>
+#include <xbt/automaton.h>
+#include <xbt/automaton.hpp>
 
 #include "ModelChecker.hpp"
 #include "mc_protocol.h"
@@ -22,6 +25,7 @@
 #include "mc_ignore.h"
 #include "mcer_ignore.h"
 #include "mc_exit.h"
+#include "src/mc/mc_liveness.h"
 
 using simgrid::mc::remote;
 
@@ -35,35 +39,11 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
 
 mc_server_t mc_server;
 
-struct mc_symbol_pointer_callback
-{
-  simgrid::mc::Process* process;
-  void* value;
-};
-
-static int mc_symbol_pointer_callback_evaluate(void* p)
-{
-  struct mc_symbol_pointer_callback* callback = (struct mc_symbol_pointer_callback*) p;
-  int value;
-  callback->process->read_bytes(&value, sizeof(value), remote(callback->value));
-  return value;
-}
-
-s_mc_server::s_mc_server(pid_t pid, int socket)
-{
-  this->pid = pid;
-  this->socket = socket;
-}
+s_mc_server::s_mc_server(pid_t pid_, int socket_)
+  : pid(pid_), socket(socket_) {}
 
 void s_mc_server::start()
 {
-  /* Wait for the target process to initialize and exchange a HELLO messages
-   * before trying to look at its memory map.
-   */
-  int res = MC_protocol_hello(socket);
-  if (res != 0)
-    throw std::system_error(res, std::system_category());
-
   // Block SIGCHLD (this will be handled with accept/signalfd):
   sigset_t set;
   sigemptyset(&set);
@@ -89,6 +69,19 @@ void s_mc_server::start()
   signalfd_pollfd->fd = signal_fd;
   signalfd_pollfd->events = POLLIN;
   signalfd_pollfd->revents = 0;
+
+  XBT_DEBUG("Waiting for the model-checked process");
+  int status;
+
+  // The model-checked process SIGSTOP itself to signal it's ready:
+  pid_t res = waitpid(pid, &status, __WALL);
+  if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
+    xbt_die("Could not wait model-checked process");
+
+  // The model-checked process is ready, we can read its memory layout:
+  MC_init_model_checker(pid, socket);
+
+  ptrace(PTRACE_CONT, pid, 0, 0);
 }
 
 void s_mc_server::shutdown()
@@ -223,15 +216,20 @@ bool s_mc_server::handle_events()
             xbt_die("Broken message");
           memcpy(&message, buffer, sizeof(message));
           if (message.callback)
-            xbt_die("Support for callbacks/functions symbols not implemented in client/server mode.");
+            xbt_die("Support for client-side function proposition is not implemented.");
           XBT_DEBUG("Received symbol: %s", message.name);
 
-          struct mc_symbol_pointer_callback* callback = xbt_new(struct mc_symbol_pointer_callback, 1);
-          callback->process = &mc_model_checker->process();
-          callback->value   = message.data;
+          if (_mc_property_automaton == NULL)
+            _mc_property_automaton = xbt_automaton_new();
+
+          simgrid::mc::Process* process = &mc_model_checker->process();
+          simgrid::mc::remote_ptr<int> address
+            = simgrid::mc::remote((int*) message.data);
+          simgrid::xbt::add_proposition(_mc_property_automaton,
+            message.name,
+            [process, address]() { return process->read(address); }
+            );
 
-          MC_automaton_new_propositional_symbol_callback(message.name,
-            mc_symbol_pointer_callback_evaluate, callback, free);
           break;
         }