#define _CRT_SECURE_NO_WARNINGS
#endif
-
-
-#ifdef _XBT_WIN32
-#define XBT_INTERNAL
-#else
-#define XBT_INTERNAL __attribute__((visibility ("hidden")))
-#endif
-
#if !defined (max) && !defined(__cplusplus)
# define max(a,b) (((a) > (b)) ? (a) : (b))
#endif
#include <string>
+#include <xbt/base.h>
+
#include "mc_forward.h"
#include "mc_location.h"
#include "mc/Variable.hpp"
#include <simgrid_config.h>
#include <xbt/dict.h>
+#include <xbt/base.h>
#include "mc_forward.hpp"
#include "mc_process.h"
#include <unordered_map>
#include <vector>
+#include <xbt/base.h>
+
#include "mc/mc_forward.h"
#include "mc/Type.hpp"
#include "mc/Frame.hpp"
#include <boost/unordered_map.hpp>
#include <boost/unordered_set.hpp>
+#include <xbt/base.h>
+
#include "mc_mmu.h"
#include "mc_forward.hpp"
#include <cstddef>
#include <utility>
+#include <xbt/base.h>
+
#include "PageStore.hpp"
#include "AddressSpace.hpp"
#include <vector>
#include <string>
+#include <xbt/base.h>
+
#include "mc_forward.h"
#include "mc_location.h"
#include <string>
+#include <xbt/base.h>
+
#include "mc_forward.h"
#include "mc_location.h"
#include "internal_config.h"
#include "../simix/smx_private.h"
-// Marker for symbols which should be defined as XBT_PRIVATE but are used in
-// unit tests:
-#define MC_SHOULD_BE_INTERNAL
-
SG_BEGIN_DECL()
/** Check if the given simcall can be resolved
*
* \return `TRUE` or `FALSE`
*/
-int MC_request_is_enabled(smx_simcall_t req);
+XBT_PRIVATE int MC_request_is_enabled(smx_simcall_t req);
/** Check if the given simcall is visible
*
* \return `TRUE` or `FALSE`
*/
-int MC_request_is_visible(smx_simcall_t req);
+XBT_PRIVATE int MC_request_is_visible(smx_simcall_t req);
/** Execute everything which is invisible
*
* iteratively until there doesn't remain any. At this point, the function
* returns to the caller which can handle the visible (and ready) simcalls.
*/
-void MC_wait_for_requests(void);
+XBT_PRIVATE void MC_wait_for_requests(void);
-XBT_INTERNAL extern double *mc_time;
+XBT_PRIVATE extern double *mc_time;
SG_END_DECL()
int fd;
} s_mc_client_t, *mc_client_t;
-extern XBT_INTERNAL mc_client_t mc_client;
+extern XBT_PRIVATE mc_client_t mc_client;
-XBT_INTERNAL void MC_client_init(void);
-XBT_INTERNAL void MC_client_hello(void);
-XBT_INTERNAL void MC_client_handle_messages(void);
-XBT_INTERNAL void MC_client_send_message(void* message, size_t size);
-XBT_INTERNAL void MC_client_send_simple_message(e_mc_message_type type);
+XBT_PRIVATE void MC_client_init(void);
+XBT_PRIVATE void MC_client_hello(void);
+XBT_PRIVATE void MC_client_handle_messages(void);
+XBT_PRIVATE void MC_client_send_message(void* message, size_t size);
+XBT_PRIVATE void MC_client_send_simple_message(e_mc_message_type type);
#ifdef HAVE_MC
void MC_ignore(void* addr, size_t size);
/**
* Type: `xbt_dynar_t<mc_list_comm_pattenr_t>`
*/
-extern XBT_INTERNAL xbt_dynar_t initial_communications_pattern;
+extern XBT_PRIVATE xbt_dynar_t initial_communications_pattern;
/**
* Type: `xbt_dynar_t<xbt_dynar_t<mc_comm_pattern_t>>`
*/
-extern XBT_INTERNAL xbt_dynar_t incomplete_communications_pattern;
+extern XBT_PRIVATE xbt_dynar_t incomplete_communications_pattern;
typedef enum {
MC_CALL_TYPE_NONE,
}
}
-XBT_INTERNAL void MC_get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking);
-XBT_INTERNAL void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t request, int value, xbt_dynar_t current_pattern, int backtracking);
-XBT_INTERNAL void MC_comm_pattern_free_voidp(void *p);
-XBT_INTERNAL void MC_list_comm_pattern_free_voidp(void *p);
-XBT_INTERNAL void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
+XBT_PRIVATE void MC_get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking);
+XBT_PRIVATE void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t request, int value, xbt_dynar_t current_pattern, int backtracking);
+XBT_PRIVATE void MC_comm_pattern_free_voidp(void *p);
+XBT_PRIVATE void MC_list_comm_pattern_free_voidp(void *p);
+XBT_PRIVATE void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
void MC_modelcheck_comm_determinism(void);
-XBT_INTERNAL void MC_restore_communications_pattern(mc_state_t state);
+XBT_PRIVATE void MC_restore_communications_pattern(mc_state_t state);
-XBT_INTERNAL mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm);
-XBT_INTERNAL xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t state);
+XBT_PRIVATE mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm);
+XBT_PRIVATE xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t state);
-XBT_INTERNAL void MC_state_copy_incomplete_communications_pattern(mc_state_t state);
-XBT_INTERNAL void MC_state_copy_index_communications_pattern(mc_state_t state);
+XBT_PRIVATE void MC_state_copy_incomplete_communications_pattern(mc_state_t state);
+XBT_PRIVATE void MC_state_copy_index_communications_pattern(mc_state_t state);
-XBT_INTERNAL void MC_comm_pattern_free(mc_comm_pattern_t p);
+XBT_PRIVATE void MC_comm_pattern_free(mc_comm_pattern_t p);
SG_END_DECL()
typedef char *type_name;
-struct s_mc_diff {
+struct XBT_PRIVATE s_mc_diff {
s_xbt_mheap_t std_heap_copy;
size_t heaplimit;
// Number of blocks in the heaps:
return a.address < b.address;
}
-XBT_INTERNAL std::shared_ptr<simgrid::mc::ObjectInformation> MC_find_object_info(
+XBT_PRIVATE std::shared_ptr<simgrid::mc::ObjectInformation> MC_find_object_info(
std::vector<simgrid::mc::VmMap> const& maps, const char* name, int executable);
-XBT_INTERNAL void MC_post_process_object_info(simgrid::mc::Process* process, simgrid::mc::ObjectInformation* info);
+XBT_PRIVATE void MC_post_process_object_info(simgrid::mc::Process* process, simgrid::mc::ObjectInformation* info);
-XBT_INTERNAL void MC_dwarf_get_variables(simgrid::mc::ObjectInformation* info);
-XBT_INTERNAL void MC_dwarf_get_variables_libdw(simgrid::mc::ObjectInformation* info);
+XBT_PRIVATE void MC_dwarf_get_variables(simgrid::mc::ObjectInformation* info);
+XBT_PRIVATE void MC_dwarf_get_variables_libdw(simgrid::mc::ObjectInformation* info);
-XBT_INTERNAL const char* MC_dwarf_attrname(int attr);
-XBT_INTERNAL const char* MC_dwarf_tagname(int tag);
+XBT_PRIVATE const char* MC_dwarf_attrname(int attr);
+XBT_PRIVATE const char* MC_dwarf_tagname(int tag);
-XBT_INTERNAL void* mc_member_resolve(
+XBT_PRIVATE void* mc_member_resolve(
const void* base, simgrid::mc::Type* type, simgrid::mc::Type* member,
simgrid::mc::AddressSpace* snapshot, int process_index);
* \param tag tag code (see the DWARF specification)
* \return name of the tag
*/
-XBT_INTERNAL
+XBT_PRIVATE
const char *MC_dwarf_tagname(int tag)
{
switch (tag) {
namespace mc {
typedef std::uint64_t hash_type;
-XBT_INTERNAL hash_type hash(simgrid::mc::Snapshot const& snapshot);
+XBT_PRIVATE hash_type hash(simgrid::mc::Snapshot const& snapshot);
}
}
SG_BEGIN_DECL();
-XBT_INTERNAL void MC_stack_area_add(stack_region_t stack_area);
+XBT_PRIVATE void MC_stack_area_add(stack_region_t stack_area);
-XBT_INTERNAL xbt_dynar_t MC_checkpoint_ignore_new(void);
+XBT_PRIVATE xbt_dynar_t MC_checkpoint_ignore_new(void);
SG_END_DECL();
SG_BEGIN_DECL()
-extern XBT_INTERNAL xbt_automaton_t _mc_property_automaton;
+extern XBT_PRIVATE xbt_automaton_t _mc_property_automaton;
-typedef struct s_mc_pair{
+typedef struct XBT_PRIVATE s_mc_pair {
int num;
int search_cycle;
mc_state_t graph_state; /* System state included */
int visited_pair_removed;
} s_mc_pair_t, *mc_pair_t;
-typedef struct s_mc_visited_pair{
+typedef struct XBT_PRIVATE s_mc_visited_pair{
int num;
int other_num; /* Dot output for */
int acceptance_pair;
int visited_removed;
} s_mc_visited_pair_t, *mc_visited_pair_t;
-XBT_INTERNAL mc_pair_t MC_pair_new(void);
-XBT_INTERNAL void MC_pair_delete(mc_pair_t);
-XBT_INTERNAL mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state);
-XBT_INTERNAL void MC_visited_pair_delete(mc_visited_pair_t p);
+XBT_PRIVATE mc_pair_t MC_pair_new(void);
+XBT_PRIVATE void MC_pair_delete(mc_pair_t);
+XBT_PRIVATE mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state);
+XBT_PRIVATE void MC_visited_pair_delete(mc_visited_pair_t p);
void MC_modelcheck_liveness(void);
-XBT_INTERNAL void MC_show_stack_liveness(xbt_fifo_t stack);
-XBT_INTERNAL void MC_dump_stack_liveness(xbt_fifo_t stack);
+XBT_PRIVATE void MC_show_stack_liveness(xbt_fifo_t stack);
+XBT_PRIVATE void MC_dump_stack_liveness(xbt_fifo_t stack);
-XBT_INTERNAL extern xbt_dynar_t visited_pairs;
-XBT_INTERNAL int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair);
+XBT_PRIVATE extern xbt_dynar_t visited_pairs;
+XBT_PRIVATE int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair);
SG_END_DECL()
}
}
-XBT_INTERNAL void mc_dwarf_resolve_location(
+XBT_PRIVATE void mc_dwarf_resolve_location(
mc_location_t location, simgrid::mc::DwarfExpression* expression,
simgrid::mc::ObjectInformation* object_info, unw_cursor_t* c,
void* frame_pointer_address, simgrid::mc::AddressSpace* address_space,
int process_index);
-MC_SHOULD_BE_INTERNAL void mc_dwarf_resolve_locations(
+void mc_dwarf_resolve_locations(
mc_location_t location, simgrid::mc::LocationList* locations,
simgrid::mc::ObjectInformation* object_info, unw_cursor_t* c,
void* frame_pointer_address, simgrid::mc::AddressSpace* address_space,
int process_index;
} s_mc_expression_state_t, *mc_expression_state_t;
-MC_SHOULD_BE_INTERNAL int mc_dwarf_execute_expression(
+int mc_dwarf_execute_expression(
size_t n, const simgrid::mc::DwarfInstruction* ops, mc_expression_state_t state);
-MC_SHOULD_BE_INTERNAL void* mc_find_frame_base(
+void* mc_find_frame_base(
simgrid::mc::Frame* frame, simgrid::mc::ObjectInformation* object_info, unw_cursor_t* unw_cursor);
SG_END_DECL()
namespace simgrid {
namespace mc {
-inline
+static inline
int execute(DwarfExpression const& expression, mc_expression_state_t state)
{
return mc_dwarf_execute_expression(
std::string pathname; /* Path name of the mapped file */
};
-std::vector<VmMap> get_memory_map(pid_t pid);
+XBT_PRIVATE std::vector<VmMap> get_memory_map(pid_t pid);
}
}
extern "C" {
-XBT_INTERNAL void MC_find_object_address(
+XBT_PRIVATE void MC_find_object_address(
std::vector<simgrid::mc::VmMap> const& maps, simgrid::mc::ObjectInformation* result);
}
#include <simgrid/msg.h>
#include "xbt/strbuff.h"
#include "xbt/parmap.h"
+#include <xbt/base.h>
#include "mc_forward.h"
#include "mc_protocol.h"
*/
void MC_init_model_checker(pid_t pid, int socket);
-XBT_INTERNAL extern FILE *dot_output;
-XBT_INTERNAL extern const char* colors[13];
-XBT_INTERNAL extern xbt_parmap_t parmap;
+XBT_PRIVATE extern FILE *dot_output;
+XBT_PRIVATE extern const char* colors[13];
+XBT_PRIVATE extern xbt_parmap_t parmap;
-XBT_INTERNAL extern int user_max_depth_reached;
+XBT_PRIVATE extern int user_max_depth_reached;
-XBT_INTERNAL int MC_deadlock_check(void);
-XBT_INTERNAL void MC_replay(xbt_fifo_t stack);
-XBT_INTERNAL void MC_replay_liveness(xbt_fifo_t stack);
-XBT_INTERNAL void MC_show_deadlock(smx_simcall_t req);
-XBT_INTERNAL void MC_show_stack_safety(xbt_fifo_t stack);
-XBT_INTERNAL void MC_dump_stack_safety(xbt_fifo_t stack);
-XBT_INTERNAL void MC_show_non_termination(void);
+XBT_PRIVATE int MC_deadlock_check(void);
+XBT_PRIVATE void MC_replay(xbt_fifo_t stack);
+XBT_PRIVATE void MC_replay_liveness(xbt_fifo_t stack);
+XBT_PRIVATE void MC_show_deadlock(smx_simcall_t req);
+XBT_PRIVATE void MC_show_stack_safety(xbt_fifo_t stack);
+XBT_PRIVATE void MC_dump_stack_safety(xbt_fifo_t stack);
+XBT_PRIVATE void MC_show_non_termination(void);
/** Stack (of `mc_state_t`) representing the current position of the
* the MC in the exploration graph
*
* It is managed by its head (`xbt_fifo_shift` and `xbt_fifo_unshift`).
*/
-XBT_INTERNAL extern xbt_fifo_t mc_stack;
+XBT_PRIVATE extern xbt_fifo_t mc_stack;
-XBT_INTERNAL int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max);
+XBT_PRIVATE int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max);
/****************************** Statistics ************************************/
unsigned long executed_transitions;
} s_mc_stats_t, *mc_stats_t;
-XBT_INTERNAL extern mc_stats_t mc_stats;
+XBT_PRIVATE extern mc_stats_t mc_stats;
-XBT_INTERNAL void MC_print_statistics(mc_stats_t stats);
+XBT_PRIVATE void MC_print_statistics(mc_stats_t stats);
/********************************** Snapshot comparison **********************************/
double stacks_comparison_time;
}s_mc_comparison_times_t, *mc_comparison_times_t;
-extern XBT_INTERNAL __thread mc_comparison_times_t mc_comp_times;
-extern XBT_INTERNAL __thread double mc_snapshot_comparison_time;
+extern XBT_PRIVATE __thread mc_comparison_times_t mc_comp_times;
+extern XBT_PRIVATE __thread double mc_snapshot_comparison_time;
-XBT_INTERNAL int snapshot_compare(void *state1, void *state2);
-XBT_INTERNAL void print_comparison_times(void);
+XBT_PRIVATE int snapshot_compare(void *state1, void *state2);
+XBT_PRIVATE void print_comparison_times(void);
//#define MC_DEBUG 1
#define MC_VERBOSE 1
/********************************** Miscellaneous **********************************/
-XBT_INTERNAL void MC_dump_stacks(FILE* file);
+XBT_PRIVATE void MC_dump_stacks(FILE* file);
-XBT_INTERNAL void MC_report_assertion_error(void);
+XBT_PRIVATE void MC_report_assertion_error(void);
-XBT_INTERNAL void MC_invalidate_cache(void);
+XBT_PRIVATE void MC_invalidate_cache(void);
SG_END_DECL()
#include "simgrid_config.h"
#include <sys/types.h>
+#include <xbt/base.h>
#include <xbt/mmalloc.h>
#ifdef HAVE_MC
/** Open a FD to a remote process memory (`/dev/$pid/mem`)
*/
-int open_vm(pid_t pid, int flags);
+XBT_PRIVATE int open_vm(pid_t pid, int flags);
}
}
SG_BEGIN_DECL()
-XBT_INTERNAL void MC_invalidate_cache(void);
+XBT_PRIVATE void MC_invalidate_cache(void);
SG_END_DECL()
void* data;
} s_mc_register_symbol_message_t, * mc_register_symbol_message_t;
-XBT_INTERNAL int MC_protocol_send(int socket, const void* message, size_t size);
-XBT_INTERNAL int MC_protocol_send_simple_message(int socket, e_mc_message_type type);
-XBT_INTERNAL int MC_protocol_hello(int socket);
-XBT_INTERNAL ssize_t MC_receive_message(int socket, void* message, size_t size, int options);
+XBT_PRIVATE int MC_protocol_send(int socket, const void* message, size_t size);
+XBT_PRIVATE int MC_protocol_send_simple_message(int socket, e_mc_message_type type);
+XBT_PRIVATE int MC_protocol_hello(int socket);
+XBT_PRIVATE ssize_t MC_receive_message(int socket, void* message, size_t size, int options);
-XBT_INTERNAL const char* MC_message_type_name(e_mc_message_type type);
-XBT_INTERNAL const char* MC_mode_name(e_mc_mode_t mode);
+XBT_PRIVATE const char* MC_message_type_name(e_mc_message_type type);
+XBT_PRIVATE const char* MC_mode_name(e_mc_mode_t mode);
SG_END_DECL()
/** Convert a string representation of the path into a array of `s_mc_record_item_t`
*/
-XBT_INTERNAL xbt_dynar_t MC_record_from_string(const char* data);
+XBT_PRIVATE xbt_dynar_t MC_record_from_string(const char* data);
/** Generate a string representation
*
* "pid0,value0;pid2,value2;pid3,value3". The value can be
* omitted is it is null.
*/
-XBT_INTERNAL char* MC_record_stack_to_string(xbt_fifo_t stack);
+XBT_PRIVATE char* MC_record_stack_to_string(xbt_fifo_t stack);
/** Dump the path represented by a given stack in the log
*/
-XBT_INTERNAL void MC_record_dump_path(xbt_fifo_t stack);
+XBT_PRIVATE void MC_record_dump_path(xbt_fifo_t stack);
// ***** Replay
* \param start Array of record item
* \item count Number of record items
*/
-XBT_INTERNAL void MC_record_replay(mc_record_item_t start, size_t count);
+XBT_PRIVATE void MC_record_replay(mc_record_item_t start, size_t count);
/** Replay a path represented by a string
*
* \param data String representation of the path
*/
-XBT_INTERNAL void MC_record_replay_from_string(const char* data);
+XBT_PRIVATE void MC_record_replay_from_string(const char* data);
-XBT_INTERNAL void MC_record_replay_init(void);
+XBT_PRIVATE void MC_record_replay_init(void);
SG_END_DECL()
#ifndef SIMGRID_MC_REQUEST_H
#define SIMGRID_MC_REQUEST_H
+#include <xbt/base.h>
+
#include <simgrid_config.h>
#include "../simix/smx_private.h"
MC_REQUEST_INTERNAL,
} e_mc_request_type_t;
-XBT_INTERNAL int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
-XBT_INTERNAL char* MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t type);
-XBT_INTERNAL unsigned int MC_request_testany_fail(smx_simcall_t req);
-/*int MC_waitany_is_enabled_by_comm(smx_req_t req, unsigned int comm);*/
-XBT_INTERNAL int MC_request_is_visible(smx_simcall_t req);
+XBT_PRIVATE int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
+XBT_PRIVATE char* MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t type);
+XBT_PRIVATE unsigned int MC_request_testany_fail(smx_simcall_t req);
+/* XBT_PRIVATE int MC_waitany_is_enabled_by_comm(smx_req_t req, unsigned int comm);*/
+XBT_PRIVATE int MC_request_is_visible(smx_simcall_t req);
/** Can this requests can be executed.
*
* have both a source and a destination yet is not enabled
* (unless timeout is enabled in the wait and enabeld in SimGridMC).
*/
-XBT_INTERNAL int MC_request_is_enabled(smx_simcall_t req);
-XBT_INTERNAL int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx);
+XBT_PRIVATE int MC_request_is_enabled(smx_simcall_t req);
+XBT_PRIVATE int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx);
/** Is the process ready to execute its simcall?
*
* This is true if the request associated with the process is ready.
*/
-XBT_INTERNAL int MC_process_is_enabled(smx_process_t process);
+XBT_PRIVATE int MC_process_is_enabled(smx_process_t process);
-XBT_INTERNAL char *MC_request_get_dot_output(smx_simcall_t req, int value);
+XBT_PRIVATE char *MC_request_get_dot_output(smx_simcall_t req, int value);
SG_END_DECL()
#include <stdint.h>
#include <simgrid_config.h>
+#include <xbt/base.h>
#include <xbt/dict.h>
#include "mc_forward.hpp"
#include "mc_state.h"
e_mc_reduce_dpor
} e_mc_reduce_t;
-extern XBT_INTERNAL e_mc_reduce_t mc_reduce_kind;
+extern XBT_PRIVATE e_mc_reduce_t mc_reduce_kind;
void MC_modelcheck_safety(void);
-typedef struct s_mc_visited_state{
+typedef struct XBT_PRIVATE s_mc_visited_state{
mc_snapshot_t system_state;
size_t heap_bytes_used;
int nb_processes;
int other_num; // dot_output for
}s_mc_visited_state_t, *mc_visited_state_t;
-extern XBT_INTERNAL xbt_dynar_t visited_states;
-XBT_INTERNAL mc_visited_state_t is_visited_state(mc_state_t graph_state);
-XBT_INTERNAL void visited_state_free(mc_visited_state_t state);
-XBT_INTERNAL void visited_state_free_voidp(void *s);
+extern XBT_PRIVATE xbt_dynar_t visited_states;
+XBT_PRIVATE mc_visited_state_t is_visited_state(mc_state_t graph_state);
+XBT_PRIVATE void visited_state_free(mc_visited_state_t state);
+XBT_PRIVATE void visited_state_free_voidp(void *s);
SG_END_DECL()
#include <sys/types.h>
#include <xbt/misc.h>
+#include <xbt/base.h>
#include "mc_process.h"
#include "mc_exit.h"
extern mc_server_t mc_server;
-XBT_INTERNAL void MC_server_wait_client(simgrid::mc::Process* process);
-XBT_INTERNAL void MC_server_simcall_handle(simgrid::mc::Process* process, unsigned long pid, int value);
+XBT_PRIVATE void MC_server_wait_client(simgrid::mc::Process* process);
+XBT_PRIVATE void MC_server_simcall_handle(simgrid::mc::Process* process, unsigned long pid, int value);
-XBT_INTERNAL void MC_server_loop(mc_server_t server);
+XBT_PRIVATE void MC_server_loop(mc_server_t server);
SG_END_DECL()
char* name;
};
-XBT_INTERNAL xbt_dynar_t MC_smx_process_info_list_new(void);
+XBT_PRIVATE xbt_dynar_t MC_smx_process_info_list_new(void);
-XBT_INTERNAL void MC_process_smx_refresh(simgrid::mc::Process* process);
+XBT_PRIVATE void MC_process_smx_refresh(simgrid::mc::Process* process);
/** Get the issuer of a simcall (`req->issuer`)
*
* @param process the MCed process
* @param req the simcall (copied in the local process)
*/
-XBT_INTERNAL smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req);
+XBT_PRIVATE smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req);
-XBT_INTERNAL const char* MC_smx_process_get_name(smx_process_t p);
-XBT_INTERNAL const char* MC_smx_process_get_host_name(smx_process_t p);
+XBT_PRIVATE const char* MC_smx_process_get_name(smx_process_t p);
+XBT_PRIVATE const char* MC_smx_process_get_host_name(smx_process_t p);
#define MC_EACH_SIMIX_PROCESS(process, code) \
if (mc_mode == MC_MODE_CLIENT) { \
}
/** Execute a given simcall */
-XBT_INTERNAL void MC_simcall_handle(smx_simcall_t req, int value);
+XBT_PRIVATE void MC_simcall_handle(smx_simcall_t req, int value);
-XBT_INTERNAL int MC_smpi_process_count(void);
+XBT_PRIVATE int MC_smpi_process_count(void);
/* ***** Resolve (local/MCer structure from remote/MCed addresses) ***** */
/** Get a local copy of the process from the process remote address */
-XBT_INTERNAL smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address);
+XBT_PRIVATE smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address);
/** Get the process info structure from the process remote address */
-XBT_INTERNAL mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address);
+XBT_PRIVATE mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address);
-XBT_INTERNAL unsigned long MC_smx_get_maxpid(void);
+XBT_PRIVATE unsigned long MC_smx_get_maxpid(void);
SG_END_DECL()
#include "../xbt/mmalloc/mmprivate.h"
#include <xbt/asserts.h>
#include <xbt/dynar.h>
+#include <xbt/base.h>
#include "mc_forward.hpp"
#include "ModelChecker.hpp"
// ***** Snapshot region
-XBT_INTERNAL void mc_region_restore_sparse(simgrid::mc::Process* process, mc_mem_region_t reg);
+XBT_PRIVATE void mc_region_restore_sparse(simgrid::mc::Process* process, mc_mem_region_t reg);
static inline __attribute__((always_inline))
void* mc_translate_address_region_chunked(uintptr_t addr, mc_mem_region_t region)
}
}
-XBT_INTERNAL mc_mem_region_t mc_get_snapshot_region(
+XBT_PRIVATE mc_mem_region_t mc_get_snapshot_region(
const void* addr, const simgrid::mc::Snapshot *snapshot, int process_index);
}
int region;
} s_local_variable_t, *local_variable_t;
-typedef struct s_mc_snapshot_stack {
+typedef struct XBT_PRIVATE s_mc_snapshot_stack {
std::vector<s_local_variable> local_variables;
s_mc_unw_context_t context;
std::vector<s_mc_stack_frame_t> stack_frames;
namespace simgrid {
namespace mc {
-class Snapshot : public AddressSpace {
+class XBT_PRIVATE Snapshot : public AddressSpace {
public:
Snapshot();
~Snapshot();
static const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot);
-XBT_INTERNAL mc_snapshot_t MC_take_snapshot(int num_state);
-XBT_INTERNAL void MC_restore_snapshot(mc_snapshot_t);
+XBT_PRIVATE mc_snapshot_t MC_take_snapshot(int num_state);
+XBT_PRIVATE void MC_restore_snapshot(mc_snapshot_t);
-XBT_INTERNAL void mc_restore_page_snapshot_region(
+XBT_PRIVATE void mc_restore_page_snapshot_region(
simgrid::mc::Process* process,
void* start_addr, simgrid::mc::PerPageCopy const& pagenos);
-MC_SHOULD_BE_INTERNAL const void* MC_region_read_fragmented(
+const void* MC_region_read_fragmented(
mc_mem_region_t region, void* target, const void* addr, size_t size);
-MC_SHOULD_BE_INTERNAL int MC_snapshot_region_memcmp(
+int MC_snapshot_region_memcmp(
const void* addr1, mc_mem_region_t region1,
const void* addr2, mc_mem_region_t region2, size_t size);
-XBT_INTERNAL int MC_snapshot_memcmp(
+XBT_PRIVATE int MC_snapshot_memcmp(
const void* addr1, mc_snapshot_t snapshot1,
const void* addr2, mc_snapshot_t snapshot2, int process_index, size_t size);
SG_END_DECL()
-XBT_INTERNAL int init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2,
+XBT_PRIVATE int init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2,
std::vector<s_mc_heap_ignore_region_t>* i1,
std::vector<s_mc_heap_ignore_region_t>* i2);
#ifndef SIMGRID_MC_STATE_H
#define SIMGRID_MC_STATE_H
+#include <xbt/base.h>
+
#include <simgrid_config.h>
#include "../simix/smx_private.h"
#include "mc_snapshot.h"
SG_BEGIN_DECL()
-extern XBT_INTERNAL mc_global_t initial_global_state;
+extern XBT_PRIVATE mc_global_t initial_global_state;
/* Possible exploration status of a process in a state */
typedef enum {
* For example WAITANY is transformes into a WAIT and TESTANY into TEST.
* See `MC_state_set_executed_request()`.
*/
-typedef struct mc_state {
+typedef struct XBT_PRIVATE mc_state {
unsigned long max_pid; /* Maximum pid at state's creation time */
mc_procstate_t proc_status; /* State's exploration status by process */
s_smx_synchro_t internal_comm; /* To be referenced by the internal_req */
xbt_dynar_t index_comm; // comm determinism verification
} s_mc_state_t, *mc_state_t;
-XBT_INTERNAL mc_state_t MC_state_new(void);
-XBT_INTERNAL void MC_state_delete(mc_state_t state, int free_snapshot);
-XBT_INTERNAL void MC_state_interleave_process(mc_state_t state, smx_process_t process);
-XBT_INTERNAL unsigned int MC_state_interleave_size(mc_state_t state);
-XBT_INTERNAL int MC_state_process_is_done(mc_state_t state, smx_process_t process);
-XBT_INTERNAL void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int value);
-XBT_INTERNAL smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value);
-XBT_INTERNAL smx_simcall_t MC_state_get_internal_request(mc_state_t state);
-XBT_INTERNAL smx_simcall_t MC_state_get_request(mc_state_t state, int *value);
-XBT_INTERNAL void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process);
+XBT_PRIVATE mc_state_t MC_state_new(void);
+XBT_PRIVATE void MC_state_delete(mc_state_t state, int free_snapshot);
+XBT_PRIVATE void MC_state_interleave_process(mc_state_t state, smx_process_t process);
+XBT_PRIVATE unsigned int MC_state_interleave_size(mc_state_t state);
+XBT_PRIVATE int MC_state_process_is_done(mc_state_t state, smx_process_t process);
+XBT_PRIVATE void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int value);
+XBT_PRIVATE smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value);
+XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(mc_state_t state);
+XBT_PRIVATE smx_simcall_t MC_state_get_request(mc_state_t state, int *value);
+XBT_PRIVATE void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process);
SG_END_DECL()
* much here.
*/
+#include <xbt/base.h>
+
#include "mc_process.h"
SG_BEGIN_DECL()
*
* It works with `void*` contexts allocated with `_UPT_create(pid)`.
*/
-extern unw_accessors_t mc_unw_vmread_accessors;
+extern XBT_PRIVATE unw_accessors_t mc_unw_vmread_accessors;
/** Virtual table for our `libunwind` implementation
*
*
* It works with the `s_mc_unw_context_t` context.
*/
-extern XBT_INTERNAL unw_accessors_t mc_unw_accessors;
+extern XBT_PRIVATE unw_accessors_t mc_unw_accessors;
// ***** Libunwind context
/** A `libunwind` context
*/
-typedef struct s_mc_unw_context {
+typedef struct XBT_PRIVATE s_mc_unw_context {
simgrid::mc::AddressSpace* address_space;
simgrid::mc::Process* process;
unw_context_t context;
} s_mc_unw_context_t, *mc_unw_context_t;
/** Initialises an already allocated context */
-XBT_INTERNAL int mc_unw_init_context(
+XBT_PRIVATE int mc_unw_init_context(
mc_unw_context_t context, simgrid::mc::Process* process, unw_context_t* c);
// ***** Libunwind cursor
/** Initialises a `libunwind` cursor */
-XBT_INTERNAL int mc_unw_init_cursor(unw_cursor_t *cursor, mc_unw_context_t context);
+XBT_PRIVATE int mc_unw_init_cursor(unw_cursor_t *cursor, mc_unw_context_t context);
SG_END_DECL()
#ifndef SIMGRID_MC_XBT_HPP
#define SIMGRID_MC_XBT_HPP
+#include <xbt/base.h>
+
#include "mc/AddressSpace.hpp"
namespace simgrid {
namespace mc {
-void read_element(AddressSpace const& as,
+XBT_PRIVATE void read_element(AddressSpace const& as,
void* local, remote_ptr<s_xbt_dynar_t> addr, size_t i, size_t len);
-std::size_t read_length(AddressSpace const& as, remote_ptr<s_xbt_dynar_t> addr);
+XBT_PRIVATE std::size_t read_length(
+ AddressSpace const& as, remote_ptr<s_xbt_dynar_t> addr);
}
}
/* 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 <xbt/base.h>
+
#include "internal_config.h"
#include "mc_dwarf.hpp"
#include "mc/mc_private.h"
// ***** Ignore heap chunks
-extern xbt_dynar_t mc_heap_comparison_ignore;
+extern XBT_PRIVATE xbt_dynar_t mc_heap_comparison_ignore;
-void heap_ignore_region_free(mc_heap_ignore_region_t r)
+XBT_PRIVATE void heap_ignore_region_free(mc_heap_ignore_region_t r)
{
xbt_free(r);
}
-void heap_ignore_region_free_voidp(void *r)
+XBT_PRIVATE void heap_ignore_region_free_voidp(void *r)
{
heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
}
-void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
+XBT_PRIVATE void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
{
if (mc_heap_comparison_ignore == NULL) {
mc_heap_comparison_ignore =
xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion);
}
-void MC_heap_region_ignore_remove(void *address, size_t size)
+XBT_PRIVATE void MC_heap_region_ignore_remove(void *address, size_t size)
{
unsigned int cursor = 0;
int start = 0;
// ***** Ignore global variables
-void MCer_ignore_global_variable(const char *name)
+XBT_PRIVATE void MCer_ignore_global_variable(const char *name)
{
simgrid::mc::Process* process = &mc_model_checker->process();
xbt_assert(!process->object_infos.empty(), "MC subsystem not initialized");
const char *subprogram_name,
simgrid::mc::ObjectInformation* info);
-void MC_ignore_local_variable(const char *var_name, const char *frame_name)
+XBT_PRIVATE void MC_ignore_local_variable(const char *var_name, const char *frame_name)
{
simgrid::mc::Process* process = &mc_model_checker->process();
if (strcmp(frame_name, "*") == 0)
}
}
-extern xbt_dynar_t stacks_areas;
+extern XBT_PRIVATE xbt_dynar_t stacks_areas;
-void MC_stack_area_add(stack_region_t stack_area)
+XBT_PRIVATE void MC_stack_area_add(stack_region_t stack_area)
{
if (stacks_areas == NULL)
stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
SG_BEGIN_DECL();
-XBT_INTERNAL void MCer_ignore_global_variable(const char *var_name);
-XBT_INTERNAL void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
-XBT_INTERNAL void MC_heap_region_ignore_remove(void *address, size_t size);
+XBT_PRIVATE void MCer_ignore_global_variable(const char *var_name);
+XBT_PRIVATE void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
+XBT_PRIVATE void MC_heap_region_ignore_remove(void *address, size_t size);
SG_END_DECL();
#include <sys/types.h>
+#include <xbt/base.h>
+
#include "mc_memory_map.h"
#include "mc_private.h"
namespace simgrid {
namespace mc {
-std::vector<VmMap> get_memory_map(pid_t pid)
+XBT_PRIVATE std::vector<VmMap> get_memory_map(pid_t pid)
{
/* Open the actual process's proc maps file and create the memory_map_t */
/* to be returned. */
* \param tag tag code (see the DWARF specification)
* \return name of the tag
*/
-XBT_INTERNAL
+XBT_PRIVATE
const char *MC_dwarf_tagname(int tag)
{
switch (tag) {
