X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/3c5b31c9766da42c82473b8c9dbf5910b74f3cb0..41626f8a47c96f54fa3b1ee61a90fb0af699dcbc:/src/mc/mc_server.cpp

diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp
index cc7c5250bb..39b15da755 100644
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -19,6 +19,7 @@
 #include "mc_protocol.h"
 #include "mc_server.h"
 #include "mc_private.h"
+#include "mc_ignore.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
 
@@ -28,28 +29,19 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
 
 mc_server_t mc_server;
 
-int MC_server_init(pid_t pid, int socket)
+struct mc_symbol_pointer_callback
 {
-  if (mc_server)
-    xbt_die("MC server already present");
-  mc_mode = MC_MODE_SERVER;
-  mc_server = new s_mc_server(pid, socket);
-  mc_server->start();
-  return 0;
-}
+  mc_process_t process;
+  void* value;
+};
 
-void MC_server_run(void)
+static int mc_symbol_pointer_callback_evaluate(void* p)
 {
-  try {
-    mc_server->resume(&mc_model_checker->process);
-    mc_server->loop();
-    mc_server->shutdown();
-    mc_server->exit();
-  }
-  catch(std::exception& e) {
-    XBT_ERROR(e.what());
-    exit(MC_SERVER_ERROR);
-  }
+  struct mc_symbol_pointer_callback* callback = (struct mc_symbol_pointer_callback*) p;
+  int value;
+  MC_process_read(callback->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
+    &value, callback->value, sizeof(value), MC_PROCESS_INDEX_ANY);
+  return value;
 }
 
 s_mc_server::s_mc_server(pid_t pid, int socket)
@@ -69,8 +61,6 @@ void s_mc_server::start()
     throw std::system_error(res, std::system_category());
   XBT_DEBUG("Greeted the MC client");
 
-  MC_init_pid(pid, socket);
-
   // Block SIGCHLD (this will be handled with accept/signalfd):
   sigset_t set;
   sigemptyset(&set);
@@ -150,7 +140,7 @@ void throw_socket_error(int fd)
 
 void s_mc_server::handle_events()
 {
-  s_mc_message_t message;
+  char buffer[MC_MESSAGE_LENGTH];
   struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
   struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
 
@@ -165,12 +155,90 @@ void s_mc_server::handle_events()
 
   if (socket_pollfd->revents) {
     if (socket_pollfd->revents & POLLIN) {
-      ssize_t size = recv(socket_pollfd->fd, &message, sizeof(message), MSG_DONTWAIT);
+
+      ssize_t size = recv(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
       if (size == -1 && errno != EAGAIN)
         throw std::system_error(errno, std::system_category());
-      else switch(message.type) {
+
+      s_mc_message_t base_message;
+      if (size < (ssize_t) sizeof(base_message))
+        xbt_die("Broken message");
+      memcpy(&base_message, buffer, sizeof(base_message));
+
+      switch(base_message.type) {
+
+      case MC_MESSAGE_IGNORE_HEAP:
+        {
+          XBT_DEBUG("Received ignored region");
+          s_mc_ignore_heap_message_t message;
+          if (size != sizeof(message))
+            xbt_die("Broken messsage");
+          memcpy(&message, buffer, sizeof(message));
+          mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
+          *region = message.region;
+          MC_heap_region_ignore_insert(region);
+          break;
+        }
+
+
+      case MC_MESSAGE_UNIGNORE_HEAP:
+        {
+          XBT_DEBUG("Received unignored region");
+          s_mc_ignore_memory_message_t message;
+          if (size != sizeof(message))
+            xbt_die("Broken messsage");
+          memcpy(&message, buffer, sizeof(message));
+          MC_remove_ignore_heap(message.addr, message.size);
+          break;
+        }
+
+      case MC_MESSAGE_IGNORE_MEMORY:
+        {
+          XBT_DEBUG("Received ignored memory");
+          s_mc_ignore_memory_message_t message;
+          if (size != sizeof(message))
+            xbt_die("Broken messsage");
+          memcpy(&message, buffer, sizeof(message));
+          MC_process_ignore_memory(&mc_model_checker->process,
+            message.addr, message.size);
+          break;
+        }
+
+      case MC_MESSAGE_STACK_REGION:
+        {
+          XBT_DEBUG("Received stack area");
+          s_mc_stack_region_message_t message;
+          if (size != sizeof(message))
+            xbt_die("Broken messsage");
+          memcpy(&message, buffer, sizeof(message));
+          stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
+          *stack_region = message.stack_region;
+          MC_stack_area_add(stack_region);
+        }
+        break;
+
+      case MC_MESSAGE_REGISTER_SYMBOL:
+        {
+          s_mc_register_symbol_message_t message;
+          if (size != sizeof(message))
+            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_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;
+
+          MC_automaton_new_propositional_symbol_callback(message.name,
+            mc_symbol_pointer_callback_evaluate, callback, free);
+          break;
+        }
+
       default:
         xbt_die("Unexpected message from model-checked application");
+
       }
       return;
     }
@@ -234,7 +302,7 @@ void s_mc_server::handle_waitpid()
         else
           break;
       } else {
-        XBT_ERROR("Could not wait for pid: %s", strerror(errno));
+        XBT_ERROR("Could not wait for pid");
         throw std::system_error(errno, std::system_category());
       }
     }