XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
-typedef struct s_mc_client {
- int active;
- int fd;
-} s_mc_client_t, mc_client_t;
-
-static s_mc_client_t mc_client;
+s_mc_client_t mc_client;
void MC_client_init(void)
{
{
while (1) {
XBT_DEBUG("Waiting messages from model-checker");
- s_mc_message_t message;
- if (recv(mc_client.fd, &message, sizeof(message), 0) == -1)
+
+ char message_buffer[MC_MESSAGE_LENGTH];
+ size_t s;
+ if ((s = recv(mc_client.fd, &message_buffer, sizeof(message_buffer), 0)) == -1)
xbt_die("Could not receive commands from the model-checker: %s",
strerror(errno));
+
XBT_DEBUG("Receive message from model-checker");
+ s_mc_message_t message;
+ if (s < sizeof(message))
+ xbt_die("Message is too short");
+ memcpy(&message, message_buffer, sizeof(message));
switch (message.type) {
case MC_MESSAGE_CONTINUE:
return;
SG_BEGIN_DECL()
+typedef struct s_mc_client {
+ int active;
+ int fd;
+} s_mc_client_t, mc_client_t;
+
+extern s_mc_client_t mc_client;
+
void MC_client_init(void);
void MC_client_hello(void);
void MC_client_handle_messages(void);
#include <xbt/log.h>
#include "mc_protocol.h"
+#include "mc_client.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_protocol, mc, "Generic MC protocol logic");
-int MC_protocol_send_simple_message(int socket, int type)
+int MC_protocol_send(int socket, void* message, size_t size)
{
- s_mc_message_t message;
- message.type = type;
-
- while (send(socket, &message, sizeof(message), 0) == -1) {
+ while (send(socket, message, size, 0) == -1) {
if (errno == EINTR)
continue;
else
return 0;
}
+int MC_protocol_send_simple_message(int socket, int type)
+{
+ s_mc_message_t message;
+ message.type = type;
+ return MC_protocol_send(socket, &message, sizeof(message));
+}
+
int MC_protocol_hello(int socket)
{
int e;
s_mc_message_t message;
message.type = MC_MESSAGE_NONE;
- while (recv(socket, &message, sizeof(message), 0) == -1) {
+ size_t s;
+ while ((s = recv(socket, &message, sizeof(message), 0)) == -1) {
if (errno == EINTR)
continue;
else {
return 2;
}
}
- if (message.type != MC_MESSAGE_HELLO) {
+ if (s < sizeof(message) || message.type != MC_MESSAGE_HELLO) {
XBT_ERROR("Did not receive suitable HELLO message. Who are you?");
return 3;
}
#include <xbt/misc.h>
+#include "mc/datatypes.h"
+
SG_BEGIN_DECL()
// ***** Environment variables for passing context to the model-checked process
// ***** Messages
-enum {
+typedef enum {
MC_MESSAGE_NONE = 0,
MC_MESSAGE_HELLO = 1,
MC_MESSAGE_CONTINUE = 2,
-};
+ MC_MESSAGE_IGNORE_REGION = 3,
+} e_mc_message_type;
+
+#define MC_MESSAGE_LENGTH 512
+/** Basic structure for a MC message
+ *
+ * The current version of the client/server protocol sends C structures over `AF_LOCAL`
+ * `SOCK_DGRAM` sockets. This means that the protocol is ABI/architecture specific:
+ * we currently can't model-check a x86 process from a x86_64 process.
+ *
+ * Moreover the protocol is not stable. The same version of the library should be used
+ * for the client and the server.
+ *
+ * This is the basic structure shared by all messages: all message start with a message
+ * type.
+ */
typedef struct s_mc_message {
- int type;
+ e_mc_message_type type;
} s_mc_message_t, *mc_message_t;
-/**
- * @return errno
- */
+typedef struct s_mc_ignore_region_message {
+ e_mc_message_type type;
+ s_mc_heap_ignore_region_t region;
+} s_mc_ignore_region_message_t, *mc_ignore_region_message_t;
+
+int MC_protocol_send(int socket, void* message, size_t size);
int MC_protocol_send_simple_message(int socket, int type);
int MC_protocol_hello(int socket);
if (size == -1 && errno != EAGAIN)
throw std::system_error(errno, std::system_category());
else switch(message.type) {
+ case MC_MESSAGE_IGNORE_REGION:
+ XBT_DEBUG("Received ignored region");
+ // Ignored for now
+ break;
default:
xbt_die("Unexpected message from model-checked application");
}