[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).

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index 94d3a08..2b699db 100644 (file)
--- 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 3c14b2a..53e1214 100644 (file)
--- 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 <stdbool.h>
 
 #include <simgrid_config.h> /* HAVE_MC ? */
 #include <xbt.h>
 #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 (file)
index 0000000..8b3827d
--- /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 <utility>
+
+#include <xbt/automaton.h>
+
+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<class F>
+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 1df6abe..5440a68 100644 (file)
--- 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 b882504..8e5f940 100644 (file)
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -14,6 +14,8 @@
 #include <sys/signalfd.h>
 
 #include <xbt/log.h>
+#include <xbt/automaton.h>
+#include <xbt/automaton.hpp>
 
 #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<int> 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;
         }