From 7b4766bf670b8042a39700c3f27e61b82db3d6cd Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sun, 31 Jul 2022 01:37:40 +0200 Subject: [PATCH] MC further cleanups (let it compile, this time) --- MANIFEST.in | 1 - include/simgrid/modelchecker.h | 20 +++------------ src/kernel/context/ContextUnix.cpp | 7 +++-- src/mc/Session.hpp | 2 +- src/mc/api.cpp | 1 - src/mc/api/State.hpp | 2 +- src/mc/mc_client_api.cpp | 41 ------------------------------ src/mc/mc_ignore.hpp | 19 -------------- src/mc/remote/AppSide.cpp | 18 +++++++++++++ tools/cmake/DefinePackages.cmake | 1 - 10 files changed, 27 insertions(+), 85 deletions(-) delete mode 100644 src/mc/mc_ignore.hpp diff --git a/MANIFEST.in b/MANIFEST.in index d9946cdc1a..a1b8d5ad8d 100644 --- 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 ea97b21955..c61a45db98 100644 --- 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 24b2b1f34d..98f78320de 100644 --- 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&& 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 c895a34258..16294c87c4 100644 --- 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 diff --git a/src/mc/api.cpp b/src/mc/api.cpp index e097a37de8..f854af4da5 100644 --- 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 49317bc119..ddca326a70 100644 --- 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 d8044c33d2..3897cf2e64 100644 --- 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 index 55e725409d..0000000000 --- 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 /* 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 c361f58603..eaf261bacc 100644 --- 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 f603a1cf67..5be7c8a2a7 100644 --- 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 -- 2.20.1