From fe9ec44b78f1d4b5a89db951d025bb33d0cd73d1 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Fri, 6 Feb 2015 14:58:15 +0100 Subject: [PATCH] (wip) Move the MCed public API in the same file --- buildtools/Cmake/DefinePackages.cmake | 1 + include/simgrid/modelchecker.h | 22 ++++---- src/mc/mc_checkpoint.c | 5 -- src/mc/mc_client.c | 18 ------- src/mc/mc_client_api.c | 76 +++++++++++++++++++++++++++ src/mc/mc_compare.cpp | 16 ------ src/mc/mc_global.c | 19 ------- 7 files changed, 88 insertions(+), 69 deletions(-) create mode 100644 src/mc/mc_client_api.c diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index 64e279fa49..76cc745f56 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -643,6 +643,7 @@ set(MC_SRC src/mc/mc_memory_map.h src/mc/memory_map.c src/mc/mc_client.c + src/mc/mc_client_api.c src/mc/mc_client.h src/mc/mc_protocol.h src/mc/mc_protocol.c diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index 0d41344468..b2ce3550b2 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -17,6 +17,17 @@ SG_BEGIN_DECL() +/** Replay path (if any) in string representation + * + * This is a path as generated by `MC_record_stack_to_string()`. + */ +XBT_PUBLIC_DATA(char*) MC_record_path; + +/** Whether the replay mode is enabled */ +static inline bool MC_record_replay_is_active(void) { + return MC_record_path; +} + XBT_PUBLIC(int) MC_random(int min, int max); #ifdef HAVE_MC @@ -48,17 +59,6 @@ XBT_PUBLIC(void) MC_ignore(void *addr, size_t size); #endif -/** Replay path (if any) in string representation - * - * This is a path as generated by `MC_record_stack_to_string()`. - */ -XBT_PUBLIC_DATA(char*) MC_record_path; - -/** Whether the replay mode is enabled */ -static inline bool MC_record_replay_is_active(void) { - return MC_record_path; -} - SG_END_DECL() #endif /* SIMGRID_MODELCHECKER_H */ diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index fe602a4a00..82e88c3032 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -844,8 +844,3 @@ mc_snapshot_t simcall_HANDLER_mc_snapshot(smx_simcall_t simcall) { return MC_take_snapshot(1); } - -void *MC_snapshot(void) -{ - return simcall_mc_snapshot(); -} diff --git a/src/mc/mc_client.c b/src/mc/mc_client.c index c903246cce..6a8d4eeb07 100644 --- a/src/mc/mc_client.c +++ b/src/mc/mc_client.c @@ -92,21 +92,3 @@ void MC_client_handle_messages(void) } } } - -void MC_ignore(void* addr, size_t size) -{ - if (mc_mode == MC_MODE_CLIENT) { - s_mc_ignore_memory_message_t message; - message.type = MC_MESSAGE_IGNORE_MEMORY; - message.addr = addr; - message.size = size; - MC_client_send_message(&message, sizeof(message)); - } - - // TODO, remove this once the migration has been completed - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_MC_HEAP; - MC_process_ignore_memory(&mc_model_checker->process, addr, size); - if (!raw_mem_set) - MC_SET_STD_HEAP; -} diff --git a/src/mc/mc_client_api.c b/src/mc/mc_client_api.c new file mode 100644 index 0000000000..9c7b2e7619 --- /dev/null +++ b/src/mc/mc_client_api.c @@ -0,0 +1,76 @@ +/* Copyright (c) 2008-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. */ + +#include +#include +#include +#include + +#include "mc_record.h" +#include "mc_private.h" +#include "mc_mmalloc.h" +#include "mc_model_checker.h" +#include "mc_ignore.h" +#include "mc_protocol.h" +#include "mc_client.h" + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc, + "Public API for the model-checked application"); + +void MC_assert(int prop) +{ + if (MC_is_active() && !prop) { + XBT_INFO("**************************"); + XBT_INFO("*** PROPERTY NOT VALID ***"); + XBT_INFO("**************************"); + XBT_INFO("Counter-example execution trace:"); + MC_record_dump_path(mc_stack); + MC_dump_stack_safety(mc_stack); + MC_print_statistics(mc_stats); + xbt_abort(); + } +} + +// TODO, MC_automaton_new_propositional_symbol + +void *MC_snapshot(void) +{ + return simcall_mc_snapshot(); +} + +int simcall_HANDLER_mc_compare_snapshots(smx_simcall_t simcall, + mc_snapshot_t s1, mc_snapshot_t s2) +{ + return snapshot_compare(s1, s2); +} + +int MC_compare_snapshots(void *s1, void *s2) +{ + return simcall_mc_compare_snapshots(s1, s2); +} + +void MC_cut(void) +{ + user_max_depth_reached = 1; +} + +void MC_ignore(void* addr, size_t size) +{ + if (mc_mode == MC_MODE_CLIENT) { + s_mc_ignore_memory_message_t message; + message.type = MC_MESSAGE_IGNORE_MEMORY; + message.addr = addr; + message.size = size; + MC_client_send_message(&message, sizeof(message)); + } + + // TODO, remove this once the migration has been completed + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); + MC_SET_MC_HEAP; + MC_process_ignore_memory(&mc_model_checker->process, addr, size); + if (!raw_mem_set) + MC_SET_STD_HEAP; +} diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp index 55db66055c..5b6352ade7 100644 --- a/src/mc/mc_compare.cpp +++ b/src/mc/mc_compare.cpp @@ -713,20 +713,4 @@ void print_comparison_times() XBT_DEBUG("- Stacks : %f", mc_comp_times->stacks_comparison_time); } -/**************************** MC snapshot compare simcall **************************/ -/***********************************************************************************/ - -int simcall_HANDLER_mc_compare_snapshots(smx_simcall_t simcall, - mc_snapshot_t s1, mc_snapshot_t s2) -{ - return snapshot_compare(s1, s2); -} - -int MC_compare_snapshots(void *s1, void *s2) -{ - - return simcall_mc_compare_snapshots(s1, s2); - -} - } diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 22b7535d83..178fee19eb 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -730,25 +730,6 @@ void MC_print_statistics(mc_stats_t stats) mmalloc_set_current_heap(previous_heap); } -void MC_assert(int prop) -{ - if (MC_is_active() && !prop) { - XBT_INFO("**************************"); - XBT_INFO("*** PROPERTY NOT VALID ***"); - XBT_INFO("**************************"); - XBT_INFO("Counter-example execution trace:"); - MC_record_dump_path(mc_stack); - MC_dump_stack_safety(mc_stack); - MC_print_statistics(mc_stats); - xbt_abort(); - } -} - -void MC_cut(void) -{ - user_max_depth_reached = 1; -} - void MC_automaton_load(const char *file) { -- 2.20.1