From: Gabriel Corona Date: Tue, 10 Feb 2015 11:19:20 +0000 (+0100) Subject: [mc] Extend xbt_propositional_symbols X-Git-Tag: v3_12~732^2~124 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/fb38ec7f242abb0362371bbdd3cb848d3e1d1303 [mc] Extend xbt_propositional_symbols Add support for: * general callbacks with a `void*` argument (the `data` field); * as an optimisation, a simple pointer to a variable can be passed in the `data` field (this can be used in order to enable the MCer to fetch the data directly from the MCed memory without trigerring a MCed-side callback); * a callback function used to free the `data` field. --- diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index b2ce3550b2..cc1888eca0 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -39,7 +39,7 @@ extern int _sg_mc_visited; #define MC_visited_reduction() _sg_mc_visited XBT_PUBLIC(void) MC_assert(int); -XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct); +XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, int(*fct)(void)); XBT_PUBLIC(void *) MC_snapshot(void); XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2); XBT_PUBLIC(void) MC_cut(void); diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h index c24453f727..ade3328389 100644 --- a/include/xbt/automaton.h +++ b/include/xbt/automaton.h @@ -57,10 +57,7 @@ typedef struct xbt_automaton_transition { typedef struct xbt_automaton_transition* xbt_automaton_transition_t; -typedef struct xbt_automaton_propositional_symbol{ - char* pred; - void* function; -} s_xbt_automaton_propositional_symbol; +typedef struct xbt_automaton_propositional_symbol s_xbt_automaton_propositional_symbol; typedef struct xbt_automaton_propositional_symbol* xbt_automaton_propositional_symbol_t; @@ -99,7 +96,11 @@ XBT_PUBLIC(void) xbt_automaton_display(xbt_automaton_t a); XBT_PUBLIC(void) xbt_automaton_exp_label_display(xbt_automaton_exp_label_t l); -XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, void* fct); +XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, int(*fct)(void)); + +XBT_PUBLIC(int) xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol); + +char* xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol); XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_get_current_state(xbt_automaton_t a); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 27c83bd75e..9b29b4e0de 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -699,7 +699,7 @@ void MC_automaton_load(const char *file) mmalloc_set_current_heap(heap); } -void MC_automaton_new_propositional_symbol(const char *id, void *fct) +void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void)) { xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 3799185bed..d7f46a1296 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -28,15 +28,12 @@ xbt_parmap_t parmap; static xbt_dynar_t get_atomic_propositions_values() { - int res; - int_f_void_t f; 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) { - f = (int_f_void_t) ps->function; - res = f(); + int res = xbt_automaton_propositional_symbol_evaluate(ps); xbt_dynar_push_as(values, int, res); } @@ -185,7 +182,7 @@ static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_automaton_propositional_symbol_t p = NULL; xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p) { - if (strcmp(p->pred, l->u.predicat) == 0) + if (strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0) return (int) xbt_dynar_get_as(atomic_propositions_values, cursor, int); } diff --git a/src/xbt/automaton/automaton.c b/src/xbt/automaton/automaton.c index 5c63609816..43f389c2a5 100644 --- a/src/xbt/automaton/automaton.c +++ b/src/xbt/automaton/automaton.c @@ -9,6 +9,30 @@ #include "xbt/automaton.h" #include /* printf */ +struct xbt_automaton_propositional_symbol{ + char* pred; + /** Callback used to evaluate the value of the symbol */ + int (*function)(void*); + /** Additional data for the callback. + Alternatively it can be used as a pointer to the data. */ + void* data; + //** Optional callback used to free the data field */ + 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); @@ -197,11 +221,18 @@ xbt_automaton_state_t xbt_automaton_get_current_state(xbt_automaton_t a){ return a->current_state; } -xbt_automaton_propositional_symbol_t xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, void* fct){ +static int call_simple_function(void* function) +{ + return ((int (*)(void)) function)(); +} + +xbt_automaton_propositional_symbol_t xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, int(*fct)(void)){ 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 = fct; + prop_symb->function = call_simple_function; + prop_symb->data = fct; + prop_symb->free_function = NULL; xbt_dynar_push(a->propositional_symbols, &prop_symb); return prop_symb; } @@ -354,7 +385,11 @@ static void xbt_automaton_propositional_symbol_free(xbt_automaton_propositional_ } void xbt_automaton_propositional_symbol_free_voidp(void *ps){ - xbt_automaton_propositional_symbol_free((xbt_automaton_propositional_symbol_t) * (void **) ps); + xbt_automaton_propositional_symbol_t symbol = (xbt_automaton_propositional_symbol_t) * (void **) ps; + if (symbol->free_function) + symbol->free_function(symbol->data); + xbt_free(symbol->pred); + xbt_automaton_propositional_symbol_free(symbol); } void xbt_automaton_free(xbt_automaton_t a){