From ab1a5770e72e90720fb1f2dc0901cda2573b208b Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Fri, 24 Jul 2015 12:28:04 +0200 Subject: [PATCH] [mc] Remove MC_automaton_new_propositional_symbol_callback() It was defined in the simulated-process API and but it could not be used in this context: it was to be called in the model-checker process. Removed a lot of boilerplate callback management stuff: replaced with C++-style code (passing lambdas/functors). --- buildtools/Cmake/DefinePackages.cmake | 1 + include/simgrid/modelchecker.h | 12 +++------ include/xbt/automaton.hpp | 38 +++++++++++++++++++++++++++ src/mc/mc_global.cpp | 11 -------- src/mc/mc_server.cpp | 32 +++++++++------------- 5 files changed, 56 insertions(+), 38 deletions(-) create mode 100644 include/xbt/automaton.hpp diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index 94d3a08ac0..2b699db20e 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -698,6 +698,7 @@ set(headers_to_install include/xbt/RngStream.h include/xbt/asserts.h include/xbt/automaton.h + include/xbt/automaton.hpp include/xbt/base.h include/xbt/config.h include/xbt/cunit.h diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index 3c14b2ad9e..53e1214533 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -12,15 +12,15 @@ * with the MC. */ +#ifndef SIMGRID_MODELCHECKER_H +#define SIMGRID_MODELCHECKER_H + #include #include /* HAVE_MC ? */ #include #include "xbt/automaton.h" -#ifndef SIMGRID_MODELCHECKER_H -#define SIMGRID_MODELCHECKER_H - SG_BEGIN_DECL() XBT_PUBLIC(int) MC_random(int min, int max); @@ -44,9 +44,7 @@ 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); @@ -60,8 +58,6 @@ XBT_PUBLIC(void) MC_ignore(void *addr, size_t size); #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) diff --git a/include/xbt/automaton.hpp b/include/xbt/automaton.hpp new file mode 100644 index 0000000000..8b3827db57 --- /dev/null +++ b/include/xbt/automaton.hpp @@ -0,0 +1,38 @@ +/* Copyright (c) 2015. The SimGrid Team. + * All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef _XBT_AUTOMATON_HPP +#define _XBT_AUTOMATON_HPP + +#include + +#include + +namespace simgrid { +namespace xbt { + +/** Add a proposition to an automaton (the C++ way) + * + * This API hides all the callback and dynamic allocation hell from + * the used which can use C++ style functors and lambda expressions. + */ +template +xbt_automaton_propositional_symbol_t add_proposition( + xbt_automaton_t a, const char* id, F f) +{ + F* callback = new F(std::move(f)); + return xbt_automaton_propositional_symbol_new_callback( + a, id, + [](void* callback) -> int { return (*(F*)callback)(); }, + callback, + [](void* callback) -> void { delete (F*)callback; } + ); +} + +} +} + +#endif diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 1df6abea12..5440a688e3 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -549,17 +549,6 @@ void MC_automaton_new_propositional_symbol_pointer(const char *id, int* value) register_symbol(symbol); } -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) -{ - 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); -} - // TODO, fix cross-process access (this function is not used) void MC_dump_stacks(FILE* file) { diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp index b8825045c8..8e5f940b9b 100644 --- a/src/mc/mc_server.cpp +++ b/src/mc/mc_server.cpp @@ -14,6 +14,8 @@ #include #include +#include +#include #include "ModelChecker.hpp" #include "mc_protocol.h" @@ -22,6 +24,7 @@ #include "mc_ignore.h" #include "mcer_ignore.h" #include "mc_exit.h" +#include "mc/mc_liveness.h" using simgrid::mc::remote; @@ -35,20 +38,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic"); mc_server_t mc_server; -struct mc_symbol_pointer_callback -{ - simgrid::mc::Process* 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; - callback->process->read_bytes(&value, sizeof(value), remote(callback->value)); - return value; -} - s_mc_server::s_mc_server(pid_t pid, int socket) { this->pid = pid; @@ -226,12 +215,17 @@ bool s_mc_server::handle_events() 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; + if (_mc_property_automaton == NULL) + _mc_property_automaton = xbt_automaton_new(); + + simgrid::mc::Process* process = &mc_model_checker->process(); + simgrid::mc::remote_ptr address + = simgrid::mc::remote((int*) message.data); + simgrid::xbt::add_proposition(_mc_property_automaton, + message.name, + [process, address]() { return process->read(address); } + ); - MC_automaton_new_propositional_symbol_callback(message.name, - mc_symbol_pointer_callback_evaluate, callback, free); break; } -- 2.20.1