MC further cleanups (let it compile, this time)

diff --git a/MANIFEST.in b/MANIFEST.in
index d9946cd..a1b8d5a 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2325,7 +2325,6 @@ include src/mc/mc_forward.hpp
 include src/mc/mc_global.cpp
 include src/mc/mc_hash.cpp
 include src/mc/mc_hash.hpp
-include src/mc/mc_ignore.hpp
 include src/mc/mc_mmu.hpp
 include src/mc/mc_private.hpp
 include src/mc/mc_record.cpp

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index ea97b21..c61a45d 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -5,12 +5,6 @@
 /* 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. */
 
-/** \file modelchecker.h
- *
- *  This is the API used by the user simulated program to communicate
- *  with the MC.
- */
-
 #ifndef SIMGRID_MODELCHECKER_H
 #define SIMGRID_MODELCHECKER_H
 
@@ -26,9 +20,7 @@ XBT_PUBLIC int MC_random(int min, int max);
 
 #if SIMGRID_HAVE_MC
 
-/* Internal variable used to check if we're running under the MC
- *
- * Please don't use directly: you should use MC_is_active. */
+/* Internal variable used to check if we're running under the MC. Please use MC_is_active instead. */
 extern XBT_PUBLIC int _sg_do_model_check;
 extern XBT_PUBLIC int _sg_mc_max_visited_states;
 
@@ -44,11 +36,8 @@ 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_ignore(void* addr, size_t size);
-
 XBT_PUBLIC void MC_ignore_heap(void* address, size_t size);
 XBT_PUBLIC void MC_unignore_heap(void* address, size_t size);
-XBT_PUBLIC void MC_ignore_global_variable(const char* var_name);
 
 #else
 
@@ -56,13 +45,12 @@ XBT_PUBLIC void MC_ignore_global_variable(const char* var_name);
 #define MC_visited_reduction()          0
 
 #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_ignore(a, b)                 ((void)0)
 
-#define MC_ignore_heap(a,s)             ((void)0)
-#define MC_remove_ignore_heap(a,s)      ((void)0)
-#define MC_ignore_global_variable(v)    ((void)0)
+#define MC_ignore_heap(a, s) ((void)0)
+#define MC_unignore_heap(a, s) ((void)0)
 
 #endif
 

diff --git a/src/kernel/context/ContextUnix.cpp b/src/kernel/context/ContextUnix.cpp
index 24b2b1f..98f7832 100644 (file)
--- a/src/kernel/context/ContextUnix.cpp
+++ b/src/kernel/context/ContextUnix.cpp
@@ -8,7 +8,7 @@
 #include "mc/mc.h"
 #include "simgrid/Exception.hpp"
 #include "src/kernel/actor/ActorImpl.hpp"
-#include "src/mc/mc_ignore.hpp"
+#include "src/mc/remote/AppSide.hpp"
 
 #include "ContextUnix.hpp"
 
@@ -62,9 +62,8 @@ UContext::UContext(std::function<void()>&& code, actor::ActorImpl* actor, Swappe
     makecontext(&this->uc_, (void (*)())sysv_ctx_wrapper, 2, ctx_addr[0], ctx_addr[1]);
 
 #if SIMGRID_HAVE_MC
-    if (MC_is_active()) {
-      MC_register_stack_area(get_stack(), &(this->uc_), stack_size);
-    }
+    if (MC_is_active())
+      simgrid::mc::AppSide::get()->declare_stack(get_stack(), stack_size, &uc_);
 #endif
   }
 }

diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
index c895a34..16294c8 100644 (file)
--- a/src/mc/Session.hpp
+++ b/src/mc/Session.hpp
@@ -6,9 +6,9 @@
 #ifndef SIMGRID_MC_SESSION_HPP
 #define SIMGRID_MC_SESSION_HPP
 
-#include "mc_pattern.hpp"
 #include "simgrid/forward.h"
 #include "src/mc/ModelChecker.hpp"
+#include "src/mc/api/ActorState.hpp"
 #include "src/mc/remote/RemotePtr.hpp"
 
 #include <functional>

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index e097a37..f854af4 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -12,7 +12,6 @@
 #include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_base.hpp"
 #include "src/mc/mc_exit.hpp"
-#include "src/mc/mc_pattern.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/remote/RemoteProcess.hpp"
 #include "src/surf/HostImpl.hpp"

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index 49317bc..ddca326 100644 (file)
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -6,7 +6,7 @@
 #ifndef SIMGRID_MC_STATE_HPP
 #define SIMGRID_MC_STATE_HPP
 
-#include "src/mc/mc_pattern.hpp"
+#include "src/mc/api/ActorState.hpp"
 #include "src/mc/sosp/Snapshot.hpp"
 #include "src/mc/transition/Transition.hpp"
 

diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp
index d8044c3..3897cf2 100644 (file)
--- a/src/mc/mc_client_api.cpp
+++ b/src/mc/mc_client_api.cpp
@@ -5,7 +5,6 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/ModelChecker.hpp"
-#include "src/mc/mc_ignore.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_record.hpp"
 #include "src/mc/mc_replay.hpp"
@@ -31,14 +30,6 @@ void MC_assert(int prop)
   }
 }
 
-void MC_ignore(void* addr, size_t size)
-{
-  xbt_assert(mc_model_checker == nullptr);
-  if (not MC_is_active())
-    return;
-  simgrid::mc::AppSide::get()->ignore_memory(addr, size);
-}
-
 void MC_automaton_new_propositional_symbol(const char* /*id*/, int (*/*fct*/)())
 {
   xbt_assert(mc_model_checker == nullptr);
@@ -56,46 +47,14 @@ void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
   simgrid::mc::AppSide::get()->declare_symbol(name, value);
 }
 
-/** @brief Register a stack in the model checker
- *
- *  The stacks are allocated in the heap. The MC handle them specifically
- *  when we analyze/compare the content of the heap so it must be told where
- *  they are with this function.
- *
- *  @param stack Where the stack is
- *  @param actor Actor owning the stack
- *  @param context The context associated to that stack
- *  @param size    Size of the stack
- */
-void MC_register_stack_area(void* stack, ucontext_t* context, size_t size)
-{
-  xbt_assert(mc_model_checker == nullptr);
-  if (not MC_is_active())
-    return;
-  simgrid::mc::AppSide::get()->declare_stack(stack, size, context);
-}
-
-void MC_ignore_global_variable(const char* /*name*/)
-{
-  xbt_assert(mc_model_checker == nullptr);
-  if (not MC_is_active())
-    return;
-  // TODO, send a message to the model_checker
-  xbt_die("Unimplemented");
-}
-
 void MC_ignore_heap(void *address, size_t size)
 {
   xbt_assert(mc_model_checker == nullptr);
-  if (not MC_is_active())
-    return;
   simgrid::mc::AppSide::get()->ignore_heap(address, size);
 }
 
 void MC_unignore_heap(void* address, size_t size)
 {
   xbt_assert(mc_model_checker == nullptr);
-  if (not MC_is_active())
-    return;
   simgrid::mc::AppSide::get()->unignore_heap(address, size);
 }

diff --git a/src/mc/mc_ignore.hpp b/src/mc/mc_ignore.hpp
deleted file mode 100644 (file)
index 55e7254..0000000
--- a/src/mc/mc_ignore.hpp
+++ /dev/null
@@ -1,19 +0,0 @@
-/* Copyright (c) 2015-2022. 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 SIMGRID_MC_IGNORE_HPP
-#define SIMGRID_MC_IGNORE_HPP
-
-#include "simgrid/forward.h"
-#include "src/internal_config.h"
-
-#if HAVE_UCONTEXT_H
-#include <ucontext.h> /* context relative declarations */
-
-XBT_PUBLIC void MC_register_stack_area(void* stack, ucontext_t* context, size_t size);
-
-#endif
-
-#endif

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index c361f58..eaf261b 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -232,6 +232,9 @@ void AppSide::report_assertion_failure() const
 
 void AppSide::ignore_memory(void* addr, std::size_t size) const
 {
+  if (not MC_is_active())
+    return;
+
   s_mc_message_ignore_memory_t message;
   message.type = MessageType::IGNORE_MEMORY;
   message.addr = (std::uintptr_t)addr;
@@ -241,6 +244,9 @@ void AppSide::ignore_memory(void* addr, std::size_t size) const
 
 void AppSide::ignore_heap(void* address, std::size_t size) const
 {
+  if (not MC_is_active())
+    return;
+
   const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
 
   s_mc_message_ignore_heap_t message;
@@ -261,6 +267,9 @@ void AppSide::ignore_heap(void* address, std::size_t size) const
 
 void AppSide::unignore_heap(void* address, std::size_t size) const
 {
+  if (not MC_is_active())
+    return;
+
   s_mc_message_ignore_memory_t message;
   message.type = MessageType::UNIGNORE_HEAP;
   message.addr = (std::uintptr_t)address;
@@ -280,8 +289,17 @@ void AppSide::declare_symbol(const char* name, int* value) const
   xbt_assert(channel_.send(message) == 0, "Could send REGISTER_SYMBOL message to model-checker");
 }
 
+/** Register a stack in the model checker
+ *
+ *  The stacks are allocated in the heap. The MC handle them specifically
+ *  when we analyze/compare the content of the heap so it must be told where
+ *  they are with this function.
+ */
 void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const
 {
+  if (not MC_is_active())
+    return;
+
   const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
 
   s_stack_region_t region;

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index f603a1c..5be7c8a 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -649,7 +649,6 @@ set(MC_SRC
   src/mc/mc_forward.hpp
   src/mc/mc_hash.cpp
   src/mc/mc_hash.hpp
-  src/mc/mc_ignore.hpp
   src/mc/mc_private.hpp
   src/mc/mc_record.cpp
   src/mc/mc_safety.hpp