From: Martin Quinson Date: Sun, 19 Mar 2023 13:29:05 +0000 (+0100) Subject: Move handle_message from ModelChecker to RemoteProcessMemory X-Git-Tag: v3.34~299 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/1f7ae620b5e74e6d7b364807ef04b6c869f7d744 Move handle_message from ModelChecker to RemoteProcessMemory --- diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 71a7f08aa6..0a1a07789e 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -30,82 +30,4 @@ ModelChecker::ModelChecker(std::unique_ptr remote_memory) { } -bool ModelChecker::handle_message(const char* buffer, ssize_t size) -{ - s_mc_message_t base_message; - xbt_assert(size >= (ssize_t)sizeof(base_message), "Broken message"); - memcpy(&base_message, buffer, sizeof(base_message)); - - switch(base_message.type) { - case MessageType::INITIAL_ADDRESSES: { - s_mc_message_initial_addresses_t message; - xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message)); - memcpy(&message, buffer, sizeof(message)); - - get_remote_process_memory().init(message.mmalloc_default_mdp); - break; - } - - case MessageType::IGNORE_HEAP: { - s_mc_message_ignore_heap_t message; - xbt_assert(size == sizeof(message), "Broken message"); - memcpy(&message, buffer, sizeof(message)); - - IgnoredHeapRegion region; - region.block = message.block; - region.fragment = message.fragment; - region.address = message.address; - region.size = message.size; - get_remote_process_memory().ignore_heap(region); - break; - } - - case MessageType::UNIGNORE_HEAP: { - s_mc_message_ignore_memory_t message; - xbt_assert(size == sizeof(message), "Broken message"); - memcpy(&message, buffer, sizeof(message)); - get_remote_process_memory().unignore_heap((void*)(std::uintptr_t)message.addr, message.size); - break; - } - - case MessageType::IGNORE_MEMORY: { - s_mc_message_ignore_memory_t message; - xbt_assert(size == sizeof(message), "Broken message"); - memcpy(&message, buffer, sizeof(message)); - this->get_remote_process_memory().ignore_region(message.addr, message.size); - break; - } - - case MessageType::STACK_REGION: { - s_mc_message_stack_region_t message; - xbt_assert(size == sizeof(message), "Broken message"); - memcpy(&message, buffer, sizeof(message)); - this->get_remote_process_memory().stack_areas().push_back(message.stack_region); - } break; - - case MessageType::REGISTER_SYMBOL: { - s_mc_message_register_symbol_t message; - xbt_assert(size == sizeof(message), "Broken message"); - memcpy(&message, buffer, sizeof(message)); - xbt_assert(not message.callback, "Support for client-side function proposition is not implemented."); - XBT_DEBUG("Received symbol: %s", message.name.data()); - - LivenessChecker::automaton_register_symbol(get_remote_process_memory(), message.name.data(), - remote((int*)message.data)); - break; - } - - case MessageType::WAITING: - return false; - - case MessageType::ASSERTION_FAILED: - Exploration::get_instance()->report_assertion_failure(); - break; - - default: - xbt_die("Unexpected message from model-checked application"); - } - return true; -} - } // namespace simgrid::mc diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index d75a38d4ba..41aa6cbad2 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -26,8 +26,6 @@ public: explicit ModelChecker(std::unique_ptr remote_simulation); RemoteProcessMemory& get_remote_process_memory() { return *remote_process_memory_; } - - bool handle_message(const char* buffer, ssize_t size); // FIXME move to RemoteApp }; } // namespace simgrid::mc diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp index eeaee22908..cf0d9e0ea9 100644 --- a/src/mc/remote/CheckerSide.cpp +++ b/src/mc/remote/CheckerSide.cpp @@ -31,7 +31,7 @@ CheckerSide::CheckerSide(int sockfd, ModelChecker* mc) : channel_(sockfd) throw simgrid::xbt::errno_error(); } - if (not mc_model_checker->handle_message(buffer.data(), size)) + if (not mc_model_checker->get_remote_process_memory().handle_message(buffer.data(), size)) checker->break_loop(); } else { xbt_die("Unexpected event"); diff --git a/src/mc/sosp/RemoteProcessMemory.cpp b/src/mc/sosp/RemoteProcessMemory.cpp index 1973a93e11..0bfb964fea 100644 --- a/src/mc/sosp/RemoteProcessMemory.cpp +++ b/src/mc/sosp/RemoteProcessMemory.cpp @@ -8,6 +8,7 @@ #include "src/mc/sosp/RemoteProcessMemory.hpp" #include "src/mc/explo/Exploration.hpp" +#include "src/mc/explo/LivenessChecker.hpp" #include "src/mc/sosp/Snapshot.hpp" #include "xbt/file.hpp" #include "xbt/log.h" @@ -455,6 +456,84 @@ void RemoteProcessMemory::dump_stack() const unw_destroy_addr_space(as); } +bool RemoteProcessMemory::handle_message(const char* buffer, ssize_t size) +{ + s_mc_message_t base_message; + xbt_assert(size >= (ssize_t)sizeof(base_message), "Broken message"); + memcpy(&base_message, buffer, sizeof(base_message)); + + switch (base_message.type) { + case MessageType::INITIAL_ADDRESSES: { + s_mc_message_initial_addresses_t message; + xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, + (int)sizeof(message)); + memcpy(&message, buffer, sizeof(message)); + + this->init(message.mmalloc_default_mdp); + break; + } + + case MessageType::IGNORE_HEAP: { + s_mc_message_ignore_heap_t message; + xbt_assert(size == sizeof(message), "Broken message"); + memcpy(&message, buffer, sizeof(message)); + + IgnoredHeapRegion region; + region.block = message.block; + region.fragment = message.fragment; + region.address = message.address; + region.size = message.size; + this->ignore_heap(region); + break; + } + + case MessageType::UNIGNORE_HEAP: { + s_mc_message_ignore_memory_t message; + xbt_assert(size == sizeof(message), "Broken message"); + memcpy(&message, buffer, sizeof(message)); + this->unignore_heap((void*)(std::uintptr_t)message.addr, message.size); + break; + } + + case MessageType::IGNORE_MEMORY: { + s_mc_message_ignore_memory_t message; + xbt_assert(size == sizeof(message), "Broken message"); + memcpy(&message, buffer, sizeof(message)); + this->ignore_region(message.addr, message.size); + break; + } + + case MessageType::STACK_REGION: { + s_mc_message_stack_region_t message; + xbt_assert(size == sizeof(message), "Broken message"); + memcpy(&message, buffer, sizeof(message)); + this->stack_areas().push_back(message.stack_region); + } break; + + case MessageType::REGISTER_SYMBOL: { + s_mc_message_register_symbol_t message; + xbt_assert(size == sizeof(message), "Broken message"); + memcpy(&message, buffer, sizeof(message)); + xbt_assert(not message.callback, "Support for client-side function proposition is not implemented."); + XBT_DEBUG("Received symbol: %s", message.name.data()); + + LivenessChecker::automaton_register_symbol(*this, message.name.data(), remote((int*)message.data)); + break; + } + + case MessageType::WAITING: + return false; + + case MessageType::ASSERTION_FAILED: + Exploration::get_instance()->report_assertion_failure(); + break; + + default: + xbt_die("Unexpected message from model-checked application"); + } + return true; +} + void RemoteProcessMemory::handle_waitpid() { XBT_DEBUG("Check for wait event"); diff --git a/src/mc/sosp/RemoteProcessMemory.hpp b/src/mc/sosp/RemoteProcessMemory.hpp index db5354965f..b0eaeb640b 100644 --- a/src/mc/sosp/RemoteProcessMemory.hpp +++ b/src/mc/sosp/RemoteProcessMemory.hpp @@ -63,6 +63,7 @@ public: bool running() const { return running_; } void terminate() { running_ = false; } void handle_waitpid(); + bool handle_message(const char* buffer, ssize_t size); /* ************* */ /* Low-level API */