XBT_PUBLIC(void) MC_assert(int);
XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, int(*fct)(void));
XBT_PUBLIC(void) MC_automaton_new_propositional_symbol_pointer(const char *id, int* value);
+XBT_PUBLIC(void) MC_automaton_new_propositional_symbol_callback(const char* id,
+ xbt_automaton_propositional_symbol_callback_type callback,
+ void* data, xbt_automaton_propositional_symbol_free_function_type free_function);
XBT_PUBLIC(void *) MC_snapshot(void);
XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2);
XBT_PUBLIC(void) MC_cut(void);
#define MC_assert(a) xbt_assert(a)
#define MC_automaton_new_propositional_symbol(a, b) ((void)0)
#define MC_automaton_new_propositional_symbol_pointer(a, b) ((void)0)
+#define MC_automaton_new_propositional_symbol_callback(id,callback,data,free_function) \
+ if(free_function) free_function(data);
#define MC_snapshot() ((void*)0)
#define MC_compare_snapshots(a, b) 0
#define MC_cut() ((void)0)
typedef struct xbt_automaton_propositional_symbol s_xbt_automaton_propositional_symbol;
-
typedef struct xbt_automaton_propositional_symbol* xbt_automaton_propositional_symbol_t;
+typedef int (*xbt_automaton_propositional_symbol_callback_type)(void*);
+typedef void (*xbt_automaton_propositional_symbol_free_function_type)(void*);
XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new(void);
XBT_PUBLIC(void) xbt_automaton_exp_label_display(xbt_automaton_exp_label_t l);
+// xbt_automaton_propositional_symbol constructors:
XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, int(*fct)(void));
-
XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_pointer(xbt_automaton_t a, const char* id, int* value);
-
XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_callback(
xbt_automaton_t a, const char* id,
- int(*callback)(void*), void* data, void (*free_function)(void*));
+ xbt_automaton_propositional_symbol_callback_type callback,
+ void* data, xbt_automaton_propositional_symbol_free_function_type free_function);
-XBT_PUBLIC(int) xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol);
+// xbt_automaton_propositional_symbol accessors:
+XBT_PUBLIC(xbt_automaton_propositional_symbol_callback_type) xbt_automaton_propositional_symbol_get_callback(xbt_automaton_propositional_symbol_t symbol);
+XBT_PUBLIC(void*) xbt_automaton_propositional_symbol_get_data(xbt_automaton_propositional_symbol_t symbol);
+XBT_PUBLIC(const char*) xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol);
-char* xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol);
+// xbt_automaton_propositional_symbol methods!
+XBT_PUBLIC(int) xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol);
XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
mmalloc_set_current_heap(heap);
}
+static void register_symbol(xbt_automaton_propositional_symbol_t symbol)
+{
+ if (mc_mode != MC_MODE_CLIENT)
+ return;
+ s_mc_register_symbol_message_t message;
+ message.type = MC_MESSAGE_REGISTER_SYMBOL;
+ const char* name = xbt_automaton_propositional_symbol_get_name(symbol);
+ if (strlen(name) + 1 > sizeof(message.name))
+ xbt_die("Symbol is too long");
+ strncpy(message.name, name, sizeof(message.name));
+ message.callback = xbt_automaton_propositional_symbol_get_callback(symbol);
+ message.data = xbt_automaton_propositional_symbol_get_data(symbol);
+ MC_client_send_message(&message, sizeof(message));
+}
+
void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
{
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
if (_mc_property_automaton == NULL)
_mc_property_automaton = xbt_automaton_new();
- xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct);
+ xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct);
+ register_symbol(symbol);
mmalloc_set_current_heap(heap);
}
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
if (_mc_property_automaton == NULL)
_mc_property_automaton = xbt_automaton_new();
- xbt_automaton_propositional_symbol_new_pointer(_mc_property_automaton, id, value);
+ xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_pointer(_mc_property_automaton, id, value);
+ register_symbol(symbol);
+ mmalloc_set_current_heap(heap);
+}
+
+void MC_automaton_new_propositional_symbol_callback(const char* id,
+ xbt_automaton_propositional_symbol_callback_type callback,
+ void* data, xbt_automaton_propositional_symbol_free_function_type free_function)
+{
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+ if (_mc_property_automaton == NULL)
+ _mc_property_automaton = xbt_automaton_new();
+ xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_callback(
+ _mc_property_automaton, id, callback, data, free_function);
+ register_symbol(symbol);
mmalloc_set_current_heap(heap);
}
unsigned int cursor = 0;
xbt_automaton_propositional_symbol_t ps = NULL;
xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL);
- // FIXME, cross-process support
xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps) {
int res = xbt_automaton_propositional_symbol_evaluate(ps);
xbt_dynar_push_as(values, int, res);
MC_MESSAGE_UNIGNORE_HEAP,
MC_MESSAGE_IGNORE_MEMORY,
MC_MESSAGE_STACK_REGION,
+ MC_MESSAGE_REGISTER_SYMBOL,
} e_mc_message_type;
#define MC_MESSAGE_LENGTH 512
s_stack_region_t stack_region;
} s_mc_stack_region_message_t, *mc_stack_region_message_t;
+typedef struct s_mc_register_symbol_message {
+ e_mc_message_type type;
+ char name[128];
+ int (*callback)(void*);
+ void* data;
+} s_mc_register_symbol_message_t, * mc_register_symbol_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);
mc_server_t mc_server;
+struct mc_symbol_pointer_callback
+{
+ mc_process_t 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;
+ 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)
{
this->pid = pid;
}
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");
struct xbt_automaton_propositional_symbol{
char* pred;
/** Callback used to evaluate the value of the symbol */
- int (*function)(void*);
+ int (*callback)(void*);
/** Additional data for the callback.
Alternatively it can be used as a pointer to the data. */
void* data;
void (*free_function)(void*);
};
-int xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol)
-{
- if (symbol->function)
- return (symbol->function)(symbol->data);
- else
- return *(int*) symbol->data;
-}
-
-char* xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol)
-{
- return symbol->pred;
-}
-
xbt_automaton_t xbt_automaton_new(){
xbt_automaton_t automaton = NULL;
automaton = xbt_new0(struct xbt_automaton, 1);
xbt_automaton_propositional_symbol_t prop_symb = NULL;
prop_symb = xbt_new0(struct xbt_automaton_propositional_symbol, 1);
prop_symb->pred = strdup(id);
- prop_symb->function = call_simple_function;
+ prop_symb->callback = call_simple_function;
prop_symb->data = fct;
prop_symb->free_function = NULL;
xbt_dynar_push(a->propositional_symbols, &prop_symb);
xbt_automaton_propositional_symbol_t prop_symb = NULL;
prop_symb = xbt_new0(struct xbt_automaton_propositional_symbol, 1);
prop_symb->pred = strdup(id);
- prop_symb->function = NULL;
+ prop_symb->callback = NULL;
prop_symb->data = value;
prop_symb->free_function = NULL;
xbt_dynar_push(a->propositional_symbols, &prop_symb);
XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_callback(
xbt_automaton_t a, const char* id,
- int(*callback)(void*), void* data, void (*free_function)(void*))
+ xbt_automaton_propositional_symbol_callback_type callback,
+ void* data, xbt_automaton_propositional_symbol_free_function_type free_function)
{
xbt_automaton_propositional_symbol_t prop_symb = NULL;
prop_symb = xbt_new0(struct xbt_automaton_propositional_symbol, 1);
prop_symb->pred = strdup(id);
- prop_symb->function = callback;
+ prop_symb->callback = callback;
prop_symb->data = data;
prop_symb->free_function = free_function;
xbt_dynar_push(a->propositional_symbols, &prop_symb);
return prop_symb;
}
+XBT_PUBLIC(int) xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol)
+{
+ if (symbol->callback)
+ return (symbol->callback)(symbol->data);
+ else
+ return *(int*) symbol->data;
+}
+
+XBT_PUBLIC(xbt_automaton_propositional_symbol_callback_type) xbt_automaton_propositional_symbol_get_callback(xbt_automaton_propositional_symbol_t symbol)
+{
+ return symbol->callback;
+}
+
+XBT_PUBLIC(void*) xbt_automaton_propositional_symbol_get_data(xbt_automaton_propositional_symbol_t symbol)
+{
+ return symbol->data;
+}
+
+XBT_PUBLIC(const char*) xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol)
+{
+ return symbol->pred;
+}
+
int xbt_automaton_state_compare(xbt_automaton_state_t s1, xbt_automaton_state_t s2){
/* single id for each state, id and type sufficient for comparison*/