)
set(MC_SRC_BASE
- src/mc/mc_base.c
+ src/mc/mc_base.cpp
src/mc/mc_base.h
src/mc/mc_record.h
- src/mc/mc_record.c
- src/mc/mc_config.c
- src/mc/mc_global.c
+ src/mc/mc_record.cpp
+ src/mc/mc_config.cpp
+ src/mc/mc_global.cpp
)
set(MC_SRC
src/mc/mc_address_space.h
- src/mc/mc_address_space.c
+ src/mc/mc_address_space.cpp
src/mc/mc_forward.h
src/mc/mc_process.h
- src/mc/mc_process.c
+ src/mc/mc_process.cpp
src/mc/mc_unw.h
- src/mc/mc_unw.c
- src/mc/mc_unw_vmread.c
+ src/mc/mc_unw.cpp
+ src/mc/mc_unw_vmread.cpp
src/mc/mc_mmalloc.h
src/mc/mc_model_checker.h
- src/mc/mc_model_checker.c
+ src/mc/mc_model_checker.cpp
src/mc/mc_object_info.h
- src/mc/mc_object_info.c
- src/mc/mc_checkpoint.c
+ src/mc/mc_object_info.cpp
+ src/mc/mc_checkpoint.cpp
src/mc/mc_snapshot.h
- src/mc/mc_snapshot.c
+ src/mc/mc_snapshot.cpp
src/mc/mc_page_store.h
src/mc/mc_page_store.cpp
src/mc/mc_page_snapshot.cpp
src/mc/mc_comm_pattern.h
- src/mc/mc_comm_pattern.c
- src/mc/mc_comm_determinism.c
+ src/mc/mc_comm_pattern.cpp
+ src/mc/mc_comm_determinism.cpp
src/mc/mc_compare.cpp
- src/mc/mc_diff.c
- src/mc/mc_dwarf.c
+ src/mc/mc_diff.cpp
+ src/mc/mc_dwarf.cpp
src/mc/mc_dwarf_attrnames.h
- src/mc/mc_dwarf_expression.c
+ src/mc/mc_dwarf_expression.cpp
src/mc/mc_dwarf_tagnames.h
- src/mc/mc_hash.c
- src/mc/mc_ignore.c
+ src/mc/mc_hash.cpp
+ src/mc/mc_ignore.cpp
src/mc/mc_interface.h
src/mc/mc_liveness.h
src/mc/mc_location.h
- src/mc/mc_liveness.c
- src/mc/mc_record.c
- src/mc/mc_member.c
- src/mc/mc_memory.c
- src/mc/mc_pair.c
+ src/mc/mc_liveness.cpp
+ src/mc/mc_record.cpp
+ src/mc/mc_member.cpp
+ src/mc/mc_memory.cpp
+ src/mc/mc_pair.cpp
src/mc/mc_private.h
src/mc/mc_request.h
- src/mc/mc_request.c
+ src/mc/mc_request.cpp
src/mc/mc_safety.h
- src/mc/mc_safety.c
+ src/mc/mc_safety.cpp
src/mc/mc_set.cpp
src/mc/mc_state.h
- src/mc/mc_state.c
- src/mc/mc_visited.c
+ src/mc/mc_state.cpp
+ src/mc/mc_visited.cpp
src/mc/mc_memory_map.h
- src/mc/memory_map.c
- src/mc/mc_client.c
- src/mc/mc_client_api.c
+ src/mc/memory_map.cpp
+ src/mc/mc_client.cpp
+ src/mc/mc_client_api.cpp
src/mc/mc_client.h
src/mc/mc_protocol.h
- src/mc/mc_protocol.c
+ src/mc/mc_protocol.cpp
src/mc/mc_server.cpp
src/mc/mc_server.h
src/mc/mc_smx.h
- src/mc/mc_smx.c
+ src/mc/mc_smx.cpp
)
set(MC_SIMGRID_MC_SRC
endif()
endif()
- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wextra -Wunused -Wpointer-arith -Wchar-subscripts -Wcomment -Wno-unknown-warning-option -Wformat -Wwrite-strings -Wno-unused-function -Wno-unused-parameter -Wno-strict-aliasing -Wclobbered -Wno-error=clobbered -Wno-format-nonliteral -Werror")
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wextra -Wunused -Wpointer-arith -Wchar-subscripts -Wcomment -Wformat -Wwrite-strings -Wno-unused-function -Wno-unused-parameter -Wno-strict-aliasing -Wclobbered -Wno-error=clobbered -Wno-format-nonliteral -Werror")
set(CMAKE_Fortran_FLAGS "${CMAKE_Fortran_FLAGS} -Wall") # FIXME: Q&D hack
if(HAVE_MC)
set(TEST_CFILES ${TEST_CFILES}
src/mc/mc_page_store.cpp
- src/mc/mc_snapshot.c
+ src/mc/mc_snapshot.cpp
)
set(TEST_UNITS ${TEST_UNITS}
${CMAKE_CURRENT_BINARY_DIR}/src/mc_page_store_unit.cpp
- ${CMAKE_CURRENT_BINARY_DIR}/src/mc_snapshot_unit.c
+ ${CMAKE_CURRENT_BINARY_DIR}/src/mc_snapshot_unit.cpp
)
endif()
_xbt_dynar_cursor_get(_dynar,_cursor,&_data) ; \
(_cursor)++ )
+#ifndef __cplusplus
#define xbt_dynar_foreach_ptr(_dynar,_cursor,_ptr) \
for (_xbt_dynar_cursor_first(_dynar,&(_cursor)) ; \
(_ptr = _cursor < _dynar->used ? xbt_dynar_get_ptr(_dynar,_cursor) : NULL) ; \
(_cursor)++ )
-
+#else
+#define xbt_dynar_foreach_ptr(_dynar,_cursor,_ptr) \
+ for (_xbt_dynar_cursor_first(_dynar,&(_cursor)) ; \
+ (_ptr = _cursor < _dynar->used ? (decltype(_ptr)) xbt_dynar_get_ptr(_dynar,_cursor) : NULL) ; \
+ (_cursor)++ )
+#endif
/** @} */
SG_END_DECL()
* @param swag what to iterate over
* @warning you cannot modify the \a swag while using this loop
* @hideinitializer */
+#ifndef __cplusplus
#define xbt_swag_foreach(obj,swag) \
for((obj)=xbt_swag_getFirst((swag)); \
(obj)!=NULL; \
(obj)=xbt_swag_getNext((obj),(swag)->offset))
-
+#else
+#define xbt_swag_foreach(obj,swag) \
+ for((obj)=(decltype(obj)) xbt_swag_getFirst((swag)); \
+ (obj)!=NULL; \
+ (obj)=(decltype(obj)) xbt_swag_getNext((obj),(swag)->offset))
+#endif
/**
* @brief A safe swag iterator
* @param obj the indice of the loop
#ifndef MC_ADDRESS_SPACE_H
#define MC_ADDRESS_SPACE_H
+#include <xbt/misc.h>
+
#include <stdint.h>
#include "mc_forward.h"
-// ***** Data types
+SG_BEGIN_DECL()
-typedef enum e_adress_space_read_flags {
- MC_ADDRESS_SPACE_READ_FLAGS_NONE = 0,
+// ***** Data types
- /** Avoid a copy for when the data is available in the current process.
- *
- * In this case, the return value of a MC_address_space_read might
- * be different from the provided buffer.
- */
- MC_ADDRESS_SPACE_READ_FLAGS_LAZY = 1
-} e_adress_space_read_flags_t;
+/** Options for the read() operation
+ *
+ * - MC_ADDRESS_SPACE_READ_FLAGS_LAZY, avoid a copy when the data is
+ * available in the current process. In this case, the return value
+ * of MC_address_space_read might be different from the provided one.
+ */
+typedef int adress_space_read_flags_t;
+#define MC_ADDRESS_SPACE_READ_FLAGS_NONE 0
+#define MC_ADDRESS_SPACE_READ_FLAGS_LAZY 1
/** Process index used when no process is available
*
*/
struct s_mc_address_space_class {
const void* (*read)(
- mc_address_space_t address_space, e_adress_space_read_flags_t flags,
+ mc_address_space_t address_space, adress_space_read_flags_t flags,
void* target, const void* addr, size_t size,
int process_index);
mc_process_t (*get_process)(mc_address_space_t address_space);
};
+typedef const void* (*mc_address_space_class_read_callback_t)(
+ mc_address_space_t address_space, adress_space_read_flags_t flags,
+ void* target, const void* addr, size_t size,
+ int process_index);
+typedef mc_process_t (*mc_address_space_class_get_process_callback_t)(mc_address_space_t address_space);
+
// ***** Virtual/non-final methods
/** Read data from the given address space
*
- * Dynamic dispatch.
+ * Dysnamic dispatch.
*/
static inline __attribute__((always_inline))
const void* MC_address_space_read(
- mc_address_space_t address_space, e_adress_space_read_flags_t flags,
+ mc_address_space_t address_space, adress_space_read_flags_t flags,
void* target, const void* addr, size_t size,
int process_index)
{
static inline __attribute__((always_inline))
const void* MC_address_space_get_process(mc_address_space_t address_space)
{
- return address_space->address_space_class->get_process(address_space);
+ if (address_space->address_space_class->get_process)
+ return address_space->address_space_class->get_process(address_space);
+ else
+ return NULL;
}
+SG_END_DECL()
#endif
#include "mc_server.h"
#endif
+extern "C" {
+
XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
void MC_wait_for_requests(void)
#ifdef HAVE_MC
// Fetch from MCed memory:
if (!MC_process_is_self(&mc_model_checker->process)) {
- MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ MC_process_read(&mc_model_checker->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
&temp_synchro, act, sizeof(temp_synchro),
MC_PROCESS_INDEX_ANY);
act = &temp_synchro;
#ifdef HAVE_MC
// Fetch from MCed memory:
if (!MC_process_is_self(&mc_model_checker->process)) {
- MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ MC_process_read(&mc_model_checker->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
&temp_synchro, act, sizeof(temp_synchro),
MC_PROCESS_INDEX_ANY);
act = &temp_synchro;
#ifdef HAVE_MC
s_smx_mutex_t temp_mutex;
if (!MC_process_is_self(&mc_model_checker->process)) {
- MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ MC_process_read(&mc_model_checker->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
&temp_mutex, mutex, sizeof(temp_mutex),
MC_PROCESS_INDEX_ANY);
mutex = &temp_mutex;
unsigned long accept_size = input_size - reject_size; // module*accept_size
// Use rejection in order to avoid skew
- long x;
+ unsigned long x;
do {
#ifndef _XBT_WIN32
- x = random();
+ x = (unsigned long) random();
#else
- x = rand();
+ x = (unsigned long) rand();
#endif
} while( x >= accept_size );
return min + (x % output_size);
return simcall->mc_value;
}
+
+void MC_simcall_handle(smx_simcall_t req, int value)
+{
+#ifndef HAVE_MC
+ SIMIX_simcall_handle(req, value);
+#else
+ if (MC_process_is_self(&mc_model_checker->process)) {
+ SIMIX_simcall_handle(req, value);
+ return;
+ }
+
+ unsigned i;
+ mc_smx_process_info_t pi = NULL;
+
+ xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
+ if (req == &pi->copy.simcall) {
+ MC_server_simcall_handle(&mc_model_checker->process, pi->copy.pid, value);
+ return;
+ }
+ }
+
+ xbt_die("Could not find the request");
+#endif
+}
+
+}
#ifndef MC_BASE_H
#define MC_BASE_H
+#include <xbt/misc.h>
#include <simgrid/simix.h>
#include "simgrid_config.h"
#include "internal_config.h"
/* 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. */
-#define _GNU_SOURCE
-
#include <unistd.h>
#include <string.h>
#include "mc_protocol.h"
#include "mc_smx.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
"Logging specific to mc_checkpoint");
* */
void MC_find_object_address(memory_map_t maps, mc_object_info_t result)
{
- unsigned int i = 0;
+ ssize_t i = 0;
s_map_region_t reg;
const char *name = basename(result->file_name);
while (i < maps->mapsize) {
xbt_assert(!result->start_rw,
"Multiple read-write segments for %s, not supported",
maps->regions[i].pathname);
- result->start_rw = reg.start_addr;
- result->end_rw = reg.end_addr;
+ result->start_rw = (char*) reg.start_addr;
+ result->end_rw = (char*) reg.end_addr;
// .bss is usually after the .data:
s_map_region_t *next = &(maps->regions[i + 1]);
if (next->pathname == NULL && (next->prot & PROT_WRITE)
&& next->start_addr == reg.end_addr) {
- result->end_rw = maps->regions[i + 1].end_addr;
+ result->end_rw = (char*) maps->regions[i + 1].end_addr;
}
} else if ((reg.prot & PROT_READ) && (reg.prot & PROT_EXEC)) {
xbt_assert(!result->start_exec,
"Multiple executable segments for %s, not supported",
maps->regions[i].pathname);
- result->start_exec = reg.start_addr;
- result->end_exec = reg.end_addr;
+ result->start_exec = (char*) reg.start_addr;
+ result->end_exec = (char*) reg.end_addr;
} else if ((reg.prot & PROT_READ) && !(reg.prot & PROT_EXEC)) {
xbt_assert(!result->start_ro,
"Multiple read only segments for %s, not supported",
maps->regions[i].pathname);
- result->start_ro = reg.start_addr;
- result->end_ro = reg.end_addr;
+ result->start_ro = (char*) reg.start_addr;
+ result->end_ro = (char*) reg.end_addr;
}
i++;
}
unw_word_t sp = xbt_dynar_get_as(st->stack_frames, 0, mc_stack_frame_t)->sp;
xbt_dynar_push(res, &st);
- (*snapshot)->stack_sizes =
+ (*snapshot)->stack_sizes = (size_t*)
xbt_realloc((*snapshot)->stack_sizes, (cursor + 1) * sizeof(size_t));
(*snapshot)->stack_sizes[cursor] =
(char*) current_stack->address + current_stack->size - (char*) sp;
const size_t fd_dir_path_size = 20;
char fd_dir_path[fd_dir_path_size];
- if (snprintf(fd_dir_path, fd_dir_path_size,
- "/proc/%lli/fd", (long long int) snapshot->process->pid) > fd_dir_path_size)
+ int res = snprintf(fd_dir_path, fd_dir_path_size,
+ "/proc/%lli/fd", (long long int) snapshot->process->pid);
+ xbt_assert(res >= 0);
+ if ((size_t) res > fd_dir_path_size)
xbt_die("Unexpected buffer is too small for fd_dir_path");
DIR* fd_dir = opendir(fd_dir_path);
const size_t source_size = 25;
char source[25];
- if (snprintf(source, source_size, "/proc/%lli/fd/%s",
- (long long int) snapshot->process->pid, fd_number->d_name) > source_size)
+ int res = snprintf(source, source_size, "/proc/%lli/fd/%s",
+ (long long int) snapshot->process->pid, fd_number->d_name);
+ xbt_assert(res >= 0);
+ if ((size_t) res > source_size)
xbt_die("Unexpected buffer is too small for fd %s", fd_number->d_name);
const size_t link_size = 200;
char link[200];
- int res = readlink(source, link, link_size);
+ res = readlink(source, link, link_size);
if (res<0) {
xbt_die("Could not read link for %s", source);
}
fd->number = fd_value;
fd->flags = fcntl(fd_value, F_GETFL) | fcntl(fd_value, F_GETFD) ;
fd->current_position = lseek(fd_value, 0, SEEK_CUR);
- snapshot->current_fd = xbt_realloc(snapshot->current_fd, (total_fd + 1) * sizeof(fd_infos_t));
+ snapshot->current_fd = (fd_infos_t*) xbt_realloc(snapshot->current_fd, (total_fd + 1) * sizeof(fd_infos_t));
snapshot->current_fd[total_fd] = fd;
total_fd++;
}
}
static s_mc_address_space_class_t mc_snapshot_class = {
- .read = (void*) &MC_snapshot_read
+ .read = (mc_address_space_class_read_callback_t) &MC_snapshot_read,
+ .get_process = NULL
};
mc_snapshot_t MC_take_snapshot(int num_state)
xbt_die("FD snapshot not implemented in client/server mode.");
int new_fd;
- size_t i;
- for(i=0; i < snapshot->total_fd; i++){
+ for (int i=0; i < snapshot->total_fd; i++) {
new_fd = open(snapshot->current_fd[i]->filename, snapshot->current_fd[i]->flags);
if (new_fd <0) {
{
return MC_take_snapshot(1);
}
+
+}
#include "mc_private.h" // MC_deadlock_check()
#include "mc_smx.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
mc_client_t mc_client;
xbt_die("Could not send message %i", (int) ((mc_message_t)message)->type);
}
-void MC_client_send_simple_message(int type)
+void MC_client_send_simple_message(e_mc_message_type type)
{
if (MC_protocol_send_simple_message(mc_client->fd, type))
xbt_die("Could not send message %i", type);
XBT_DEBUG("Waiting messages from model-checker");
char message_buffer[MC_MESSAGE_LENGTH];
- size_t s;
- if ((s = MC_receive_message(mc_client->fd, &message_buffer, sizeof(message_buffer), 0)) == -1)
+ ssize_t s;
+ if ((s = MC_receive_message(mc_client->fd, &message_buffer, sizeof(message_buffer), 0)) < 0)
xbt_die("Could not receive commands from the model-checker");
s_mc_message_t message;
- if (s < sizeof(message))
+ if ((size_t) s < sizeof(message))
xbt_die("Received message is too small");
memcpy(&message, message_buffer, sizeof(message));
switch (message.type) {
MC_wait_for_requests();
}
}
+
+}
#define MC_CLIENT_H
#include <xbt/misc.h>
+#include "mc_protocol.h"
SG_BEGIN_DECL()
void MC_client_hello(void);
void MC_client_handle_messages(void);
void MC_client_send_message(void* message, size_t size);
-void MC_client_send_simple_message(int type);
+void MC_client_send_simple_message(e_mc_message_type type);
#ifdef HAVE_MC
void MC_ignore(void* addr, size_t size);
#include "mc_protocol.h"
#include "mc_client.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc,
"Public API for the model-checked application");
MC_process_ignore_memory(&mc_model_checker->process, addr, size);
mmalloc_set_current_heap(heap);
}
+
+}
#include "mc_smx.h"
#include "mc_client.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
"Logging specific to MC communication determinism detection");
if (comm1->data_size != comm2->data_size)
return DATA_SIZE_DIFF;
if(comm1->data == NULL && comm2->data == NULL)
- return 0;
+ return NONE_DIFF;
if(comm1->data != NULL && comm2->data !=NULL) {
if (!memcmp(comm1->data, comm2->data, comm1->data_size))
- return 0;
+ return NONE_DIFF;
return DATA_DIFF;
}else{
return DATA_DIFF;
}
- return 0;
+ return NONE_DIFF;
}
static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
MC_SET_MC_HEAP;
- while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
+ while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != NULL) {
if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
/* We found a back-tracking point, let's loop */
XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
mmalloc_set_current_heap(heap);
}
+
+}
#include "mc_comm_pattern.h"
#include "mc_smx.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_pattern, mc,
"Logging specific to MC communication patterns");
list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int);
}
- for (int i = 0; i < MC_smx_get_maxpid(); i++) {
+ for (unsigned i = 0; i < MC_smx_get_maxpid(); i++) {
MC_patterns_copy(
xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t),
xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t)
{
state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
- int i;
- for (i=0; i < MC_smx_get_maxpid(); i++) {
+ for (unsigned i=0; i < MC_smx_get_maxpid(); i++) {
xbt_dynar_t comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
xbt_dynar_t copy = MC_comm_patterns_dup(comms);
xbt_dynar_insert_at(state->incomplete_comm_pattern, i, ©);
{
MC_list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
}
+
+}
#include <inttypes.h>
#include <boost/unordered_set.hpp>
+#include <xbt/sysdep.h>
+
#include "internal_config.h"
#include "mc_object_info.h"
#include "mc_safety.h"
#include <xbt/probes.h>
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc,
- "Logging specific to mc_compare");
-
typedef struct s_pointers_pair {
void *p1;
void *p2;
extern "C" {
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt,
+ "Logging specific to mc_compare in mc");
+
/************************** Free functions ****************************/
/********************************************************************/
#include "mc_record.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc,
"Configuration of MC");
}
#endif
+
+}
#include "mc/mc_private.h"
#include "mc/mc_snapshot.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_diff, xbt,
"Logging specific to mc_diff in mc");
state->to_ignore2 = i2;
if (state->heaplimit > state->available) {
- state->equals_to1 =
+ state->equals_to1 = (s_heap_area_t*)
realloc(state->equals_to1,
state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
sizeof(s_heap_area_t));
- state->types1 =
+ state->types1 = (s_dw_type**)
realloc(state->types1,
state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
sizeof(type_name *));
- state->equals_to2 =
+ state->equals_to2 = (s_heap_area_t*)
realloc(state->equals_to2,
state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
sizeof(s_heap_area_t));
- state->types2 =
+ state->types2 = (s_dw_type**)
realloc(state->types2,
state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
sizeof(type_name *));
void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
// This is in snapshot do not use them directly:
- const malloc_info* heapinfos1 = MC_snapshot_read_pointer(snapshot1, heapinfo_address, MC_PROCESS_INDEX_MISSING);
- const malloc_info* heapinfos2 = MC_snapshot_read_pointer(snapshot2, heapinfo_address, MC_PROCESS_INDEX_MISSING);
+ const malloc_info* heapinfos1 = (const malloc_info*) MC_snapshot_read_pointer(snapshot1, heapinfo_address, MC_PROCESS_INDEX_MISSING);
+ const malloc_info* heapinfos2 = (const malloc_info*) MC_snapshot_read_pointer(snapshot2, heapinfo_address, MC_PROCESS_INDEX_MISSING);
while (i1 <= state->heaplimit) {
- const malloc_info* heapinfo1 = MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[i1], sizeof(malloc_info));
- const malloc_info* heapinfo2 = MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[i1], sizeof(malloc_info));
+ const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[i1], sizeof(malloc_info));
+ const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[i1], sizeof(malloc_info));
if (heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type == MMALLOC_TYPE_HEAPINFO) { /* Free block */
i1 ++;
continue;
}
- const malloc_info* heapinfo2b = MC_region_read(heap_region2, &heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info));
+ const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info));
if (heapinfo2b->type != MMALLOC_TYPE_UNFRAGMENTED) {
i2++;
while (i2 <= state->heaplimit && !equal) {
- const malloc_info* heapinfo2b = MC_region_read(heap_region2, &heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info));
+ const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(
+ heap_region2, &heapinfo_temp2b, &heapinfos2[i2],
+ sizeof(malloc_info));
if (heapinfo2b->type == MMALLOC_TYPE_FREE || heapinfo2b->type == MMALLOC_TYPE_HEAPINFO) {
i2 ++;
size_t i = 1, j = 0;
for(i = 1; i <= state->heaplimit; i++) {
- const malloc_info* heapinfo1 = MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[i], sizeof(malloc_info));
+ const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
+ heap_region1, &heapinfo_temp1, &heapinfos1[i], sizeof(malloc_info));
if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED) {
if (i1 == state->heaplimit) {
if (heapinfo1->busy_block.busy_size > 0) {
XBT_DEBUG("Number of blocks/fragments not found in heap1 : %d", nb_diff1);
for (i=1; i <= state->heaplimit; i++) {
- const malloc_info* heapinfo2 = MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[i], sizeof(malloc_info));
+ const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
+ heap_region2, &heapinfo_temp2, &heapinfos2[i], sizeof(malloc_info));
if (heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED) {
if (i1 == state->heaplimit) {
if (heapinfo2->busy_block.busy_size > 0) {
}
dw_type_t subtype, subsubtype;
- int res, elm_size, i;
+ int res, elm_size;
unsigned int cursor = 0;
dw_type_t member;
const void *addr_pointed1, *addr_pointed2;;
return 0;
break;
}
- for (i = 0; i < type->element_count; i++) {
+ for (int i = 0; i < type->element_count; i++) {
// TODO, add support for variable stride (DW_AT_byte_stride)
res =
compare_heap_area_with_type(state, process_index,
} else {
pointer_level++;
if (pointer_level > 1) { /* Array of pointers */
- for (i = 0; i < (area_size / sizeof(void *)); i++) {
+ for (size_t i = 0; i < (area_size / sizeof(void *)); i++) {
addr_pointed1 = MC_snapshot_read_pointer(snapshot1, (char*) real_area1 + i * sizeof(void *), process_index);
addr_pointed2 = MC_snapshot_read_pointer(snapshot2, (char*) real_area2 + i * sizeof(void *), process_index);
if (addr_pointed1 > state->std_heap_copy.heapbase
type = type->full_type;
if (area_size != -1 && type->byte_size != area_size) {
if (area_size > type->byte_size && area_size % type->byte_size == 0) {
- for (i = 0; i < (area_size / type->byte_size); i++) {
+ for (size_t i = 0; i < (size_t)(area_size / type->byte_size); i++) {
res =
compare_heap_area_with_type(state, process_index,
(char *) real_area1 + i * type->byte_size,
cursor = 0;
xbt_dynar_foreach(type->members, cursor, member) {
// TODO, optimize this? (for the offset case)
- char *real_member1 =
+ void *real_member1 =
mc_member_resolve(real_area1, type, member, (mc_address_space_t) snapshot1, process_index);
- char *real_member2 =
+ void *real_member2 =
mc_member_resolve(real_area2, type, member, (mc_address_space_t) snapshot2, process_index);
res =
compare_heap_area_with_type(state, process_index, real_member1, real_member2,
if (member->offset == offset)
return member->subtype;
} else {
- char *real_member =
- mc_member_resolve(real_base_address, type, member, (mc_address_space_t) snapshot, process_index);
- if (real_member - (char *) real_base_address == offset)
+ void *real_member =
+ mc_member_resolve(real_base_address, type, member,
+ (mc_address_space_t) snapshot, process_index);
+ if ((char*) real_member - (char *) real_base_address == offset)
return member->subtype;
}
// This is the address of std_heap->heapinfo in the application process:
void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
- const malloc_info* heapinfos1 = MC_snapshot_read_pointer(snapshot1, heapinfo_address, process_index);
- const malloc_info* heapinfos2 = MC_snapshot_read_pointer(snapshot2, heapinfo_address, process_index);
+ const malloc_info* heapinfos1 = (const malloc_info*) MC_snapshot_read_pointer(
+ snapshot1, heapinfo_address, process_index);
+ const malloc_info* heapinfos2 = (const malloc_info*) MC_snapshot_read_pointer(
+ snapshot2, heapinfo_address, process_index);
malloc_info heapinfo_temp1, heapinfo_temp2;
}
// If either block is not in the expected area of memory:
if (((char *) area1 < (char *) state->std_heap_copy.heapbase)
- || (block1 > state->heapsize1) || (block1 < 1)
+ || (block1 > (ssize_t) state->heapsize1) || (block1 < 1)
|| ((char *) area2 < (char *) state->std_heap_copy.heapbase)
- || (block2 > state->heapsize2) || (block2 < 1)) {
+ || (block2 > (ssize_t) state->heapsize2) || (block2 < 1)) {
if (match_pairs) {
xbt_dynar_free(&previous);
}
mc_mem_region_t heap_region1 = MC_get_heap_region(snapshot1);
mc_mem_region_t heap_region2 = MC_get_heap_region(snapshot2);
- const malloc_info* heapinfo1 = MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[block1], sizeof(malloc_info));
- const malloc_info* heapinfo2 = MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[block2], sizeof(malloc_info));
+ const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
+ heap_region1, &heapinfo_temp1, &heapinfos1[block1], sizeof(malloc_info));
+ const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
+ heap_region2, &heapinfo_temp2, &heapinfos2[block2], sizeof(malloc_info));
if ((heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type==MMALLOC_TYPE_HEAPINFO)
&& (heapinfo2->type == MMALLOC_TYPE_FREE || heapinfo2->type ==MMALLOC_TYPE_HEAPINFO)) {
}
if (type_size != -1) {
- if (type_size != heapinfo1->busy_block.busy_size
- && type_size != heapinfo2->busy_block.busy_size
+ if (type_size != (ssize_t) heapinfo1->busy_block.busy_size
+ && type_size != (ssize_t) heapinfo2->busy_block.busy_size
&& (type->name == NULL || !strcmp(type->name, "struct s_smx_context"))) {
if (match_pairs) {
match_equals(state, previous);
}
#endif
+
+}
#include "mc_object_info.h"
#include "mc_private.h"
+extern "C" {
+
static void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t variable);
static void MC_register_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable);
static void MC_dwarf_register_non_global_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable);
*/
static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die * die,
Dwarf_Die * unit, dw_frame_t frame,
- const char *namespace);
+ const char *ns);
/** \brief Process a type DIE
*/
static void MC_dwarf_handle_type_die(mc_object_info_t info, Dwarf_Die * die,
Dwarf_Die * unit, dw_frame_t frame,
- const char *namespace);
+ const char *ns);
/** \brief Calls MC_dwarf_handle_die on all childrend of the given die
*
*/
static void MC_dwarf_handle_children(mc_object_info_t info, Dwarf_Die * die,
Dwarf_Die * unit, dw_frame_t frame,
- const char *namespace);
+ const char *ns);
/** \brief Handle a variable (DW_TAG_variable or other)
*
*/
static void MC_dwarf_handle_variable_die(mc_object_info_t info, Dwarf_Die * die,
Dwarf_Die * unit, dw_frame_t frame,
- const char *namespace);
+ const char *ns);
/** \brief Get the DW_TAG_type of the DIE
*
*/
static dw_type_t MC_dwarf_die_to_type(mc_object_info_t info, Dwarf_Die * die,
Dwarf_Die * unit, dw_frame_t frame,
- const char *namespace)
+ const char *ns)
{
dw_type_t type = xbt_new0(s_dw_type_t, 1);
const char *name = MC_dwarf_attr_integrate_string(die, DW_AT_name);
if (name != NULL) {
type->name =
- namespace ? bprintf("%s%s::%s", prefix, namespace,
+ ns ? bprintf("%s%s::%s", prefix, ns,
name) : bprintf("%s%s", prefix, name);
}
case DW_TAG_union_type:
case DW_TAG_class_type:
MC_dwarf_add_members(info, die, unit, type);
- char *new_namespace = namespace == NULL ? xbt_strdup(type->name)
- : bprintf("%s::%s", namespace, name);
- MC_dwarf_handle_children(info, die, unit, frame, new_namespace);
- free(new_namespace);
+ char *new_ns = ns == NULL ? xbt_strdup(type->name)
+ : bprintf("%s::%s", ns, name);
+ MC_dwarf_handle_children(info, die, unit, frame, new_ns);
+ free(new_ns);
break;
}
static void MC_dwarf_handle_type_die(mc_object_info_t info, Dwarf_Die * die,
Dwarf_Die * unit, dw_frame_t frame,
- const char *namespace)
+ const char *ns)
{
- dw_type_t type = MC_dwarf_die_to_type(info, die, unit, frame, namespace);
+ dw_type_t type = MC_dwarf_die_to_type(info, die, unit, frame, ns);
char *key = bprintf("%" PRIx64, (uint64_t) type->id);
xbt_dict_set(info->types, key, type, NULL);
static dw_variable_t MC_die_to_variable(mc_object_info_t info, Dwarf_Die * die,
Dwarf_Die * unit, dw_frame_t frame,
- const char *namespace)
+ const char *ns)
{
// Skip declarations:
if (MC_dwarf_attr_flag(die, DW_AT_declaration, false))
}
}
- if (namespace && variable->global) {
+ if (ns && variable->global) {
char *old_name = variable->name;
- variable->name = bprintf("%s::%s", namespace, old_name);
+ variable->name = bprintf("%s::%s", ns, old_name);
free(old_name);
}
// The current code needs a variable name,
static void MC_dwarf_handle_variable_die(mc_object_info_t info, Dwarf_Die * die,
Dwarf_Die * unit, dw_frame_t frame,
- const char *namespace)
+ const char *ns)
{
dw_variable_t variable =
- MC_die_to_variable(info, die, unit, frame, namespace);
+ MC_die_to_variable(info, die, unit, frame, ns);
if (variable == NULL)
return;
MC_dwarf_register_variable(info, frame, variable);
static void MC_dwarf_handle_scope_die(mc_object_info_t info, Dwarf_Die * die,
Dwarf_Die * unit, dw_frame_t parent_frame,
- const char *namespace)
+ const char *ns)
{
// TODO, handle DW_TAG_type/DW_TAG_location for DW_TAG_with_stmt
int tag = dwarf_tag(die);
if (klass == mc_tag_subprogram) {
const char *name = MC_dwarf_attr_integrate_string(die, DW_AT_name);
frame->name =
- namespace ? bprintf("%s::%s", namespace, name) : xbt_strdup(name);
+ ns ? bprintf("%s::%s", ns, name) : xbt_strdup(name);
}
frame->abstract_origin_id =
xbt_dynar_push(parent_frame->scopes, &frame);
}
// Handle children:
- MC_dwarf_handle_children(info, die, unit, frame, namespace);
+ MC_dwarf_handle_children(info, die, unit, frame, ns);
}
static void mc_dwarf_handle_namespace_die(mc_object_info_t info,
Dwarf_Die * die, Dwarf_Die * unit,
dw_frame_t frame,
- const char *namespace)
+ const char *ns)
{
const char *name = MC_dwarf_attr_integrate_string(die, DW_AT_name);
if (frame)
xbt_die("Unexpected namespace in a subprogram");
- char *new_namespace = namespace == NULL ? xbt_strdup(name)
- : bprintf("%s::%s", namespace, name);
- MC_dwarf_handle_children(info, die, unit, frame, new_namespace);
- xbt_free(new_namespace);
+ char *new_ns = ns == NULL ? xbt_strdup(name)
+ : bprintf("%s::%s", ns, name);
+ MC_dwarf_handle_children(info, die, unit, frame, new_ns);
+ xbt_free(new_ns);
}
static void MC_dwarf_handle_children(mc_object_info_t info, Dwarf_Die * die,
Dwarf_Die * unit, dw_frame_t frame,
- const char *namespace)
+ const char *ns)
{
// For each child DIE:
Dwarf_Die child;
int res;
for (res = dwarf_child(die, &child); res == 0;
res = dwarf_siblingof(&child, &child)) {
- MC_dwarf_handle_die(info, &child, unit, frame, namespace);
+ MC_dwarf_handle_die(info, &child, unit, frame, ns);
}
}
static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die * die,
Dwarf_Die * unit, dw_frame_t frame,
- const char *namespace)
+ const char *ns)
{
int tag = dwarf_tag(die);
mc_tag_class klass = MC_dwarf_tag_classify(tag);
// Type:
case mc_tag_type:
- MC_dwarf_handle_type_die(info, die, unit, frame, namespace);
+ MC_dwarf_handle_type_die(info, die, unit, frame, ns);
break;
// Subprogram or scope:
case mc_tag_subprogram:
case mc_tag_scope:
- MC_dwarf_handle_scope_die(info, die, unit, frame, namespace);
+ MC_dwarf_handle_scope_die(info, die, unit, frame, ns);
return;
// Variable:
case mc_tag_variable:
- MC_dwarf_handle_variable_die(info, die, unit, frame, namespace);
+ MC_dwarf_handle_variable_die(info, die, unit, frame, ns);
break;
case mc_tag_namespace:
- mc_dwarf_handle_namespace_die(info, die, unit, frame, namespace);
+ mc_dwarf_handle_namespace_die(info, die, unit, frame, ns);
break;
default:
dw_variable_t variable = NULL;
xbt_dynar_foreach(info->global_variables, cursor, variable) {
if (variable->type_origin) {
- variable->type = xbt_dict_get_or_null(info->types, variable->type_origin);
+ variable->type = (dw_type_t) xbt_dict_get_or_null(info->types, variable->type_origin);
}
}
}
// Attach correct namespaced name in inlined subroutine:
char *key = bprintf("%" PRIx64, (uint64_t) scope->abstract_origin_id);
- dw_frame_t abstract_origin = xbt_dict_get_or_null(info->subprograms, key);
+ dw_frame_t abstract_origin = (dw_frame_t) xbt_dict_get_or_null(info->subprograms, key);
xbt_assert(abstract_origin, "Could not lookup abstract origin %s", key);
xbt_free(key);
scope->name = xbt_strdup(abstract_origin->name);
dw_variable_t variable = NULL;
xbt_dynar_foreach(scope->variables, cursor, variable) {
if (variable->type_origin) {
- variable->type = xbt_dict_get_or_null(info->types, variable->type_origin);
+ variable->type = (dw_type_t) xbt_dict_get_or_null(info->types, variable->type_origin);
}
}
if (type->dw_type_id == NULL)
return;
- type->subtype = xbt_dict_get_or_null(info->types, type->dw_type_id);
+ type->subtype = (dw_type_t) xbt_dict_get_or_null(info->types, type->dw_type_id);
if (type->subtype == NULL)
return;
if (type->subtype->byte_size != 0)
// We need to fix in order to support C++.
dw_type_t subtype =
- xbt_dict_get_or_null(info->full_types_by_name, type->subtype->name);
+ (dw_type_t) xbt_dict_get_or_null(info->full_types_by_name, type->subtype->name);
if (subtype != NULL) {
type->subtype = subtype;
}
// Resolve full_type:
if (subtype->name && subtype->byte_size == 0) {
for (size_t i = 0; i != process->object_infos_size; ++i) {
- dw_type_t same_type =
+ dw_type_t same_type = (dw_type_t)
xbt_dict_get_or_null(process->object_infos[i]->full_types_by_name,
subtype->name);
if (same_type && same_type->name && same_type->byte_size) {
}
}
+
+}
#include "mc_object_info.h"
#include "mc_private.h"
+extern "C" {
+
static int mc_dwarf_push_value(mc_expression_state_t state, Dwarf_Off value)
{
if (state->stack_size >= MC_EXPRESSION_STACK_SIZE)
int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
mc_expression_state_t state)
{
- for (int i = 0; i != n; ++i) {
+ for (size_t i = 0; i != n; ++i) {
int error = 0;
const Dwarf_Op *op = ops + i;
uint8_t atom = op->atom;
// Address from the base address of this ELF object.
// Push the address on the stack (base_address + argument).
- case DW_OP_addr:
+ case DW_OP_addr: {
if (!state->object_info)
return MC_EXPRESSION_E_NO_BASE_ADDRESS;
if (state->stack_size == MC_EXPRESSION_STACK_SIZE)
MC_object_base_address(state->object_info) + op->number;
error = mc_dwarf_push_value(state, addr);
break;
+ }
// General constants:
// Push the constant argument on the stack.
expression->lowpc = NULL;
expression->highpc = NULL;
expression->size = len;
- expression->ops = xbt_malloc(len * sizeof(Dwarf_Op));
+ expression->ops = (Dwarf_Op*) xbt_malloc(len * sizeof(Dwarf_Op));
memcpy(expression->ops, ops, len * sizeof(Dwarf_Op));
}
}
}
+
+}
#ifndef MC_FORWARD_H
#define MC_FORWARD_H
+#include <xbt/misc.h>
#include <mc/datatypes.h>
#include "mc_interface.h"
+SG_BEGIN_DECL()
+
typedef struct s_mc_object_info s_mc_object_info_t, *mc_object_info_t;
typedef struct s_dw_type s_dw_type_t, *dw_type_t;
typedef struct s_memory_map s_memory_map_t, *memory_map_t;
typedef struct s_mc_model_checker s_mc_model_checker_t, *mc_model_checker_t;
extern mc_model_checker_t mc_model_checker;
+SG_END_DECL()
+
#endif
#include "mc_protocol.h"
#include "mc_client.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
"Logging specific to MC (global)");
}
-void MC_init()
-{
- MC_init_pid(getpid(), -1);
-}
-
static void MC_init_mode(void)
{
if (mc_mode == MC_MODE_NONE) {
}
}
+#ifdef HAVE_MC
+void MC_init()
+{
+ MC_init_pid(getpid(), -1);
+}
+
void MC_init_pid(pid_t pid, int socket)
{
/* Initialize the data structures that must be persistent across every
mmalloc_set_current_heap(heap);
}
+#endif
/******************************* Core of MC *******************************/
/**************************************************************************/
//xbt_abort();
}
+#ifdef HAVE_MC
int MC_deadlock_check()
{
if (mc_mode == MC_MODE_SERVER) {
}
return deadlock;
}
+#endif
/**
* \brief Re-executes from the state at position start all the transitions indicated by
{
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
- int value, count = 1, j;
+ int value, count = 1;
char *req_str;
smx_simcall_t req = NULL, saved_req = NULL;
xbt_fifo_item_t item, start_item;
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
// int n = xbt_dynar_length(incomplete_communications_pattern);
- int n = MC_smx_get_maxpid();
+ unsigned n = MC_smx_get_maxpid();
assert(n == xbt_dynar_length(incomplete_communications_pattern));
assert(n == xbt_dynar_length(initial_communications_pattern));
- for (j=0; j < n ; j++) {
+ for (unsigned j=0; j < n ; j++) {
xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t)->index_comm = 0;
}
MC_print_statistics(mc_stats);
}
#endif
+
+}
#include "mc/datatypes.h"
#include <mc/mc.h>
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_hash, mc, "Logging specific to mc_hash");
// This is djb2:
// #define MC_HASH(hash, value) hash = (((hash << 5) + hash) + (uint64_t) value)
#define MC_HASH(hash, value) \
{ hash = (((hash << 5) + hash) + (uint64_t) value);\
- XBT_DEBUG("%s:%i: %"PRIx64" -> %"PRIx64, __FILE__, __LINE__, (uint64_t) value, hash); }
+ XBT_DEBUG("%s:%i: %" PRIx64 " -> %" PRIx64, __FILE__, __LINE__, (uint64_t) value, hash); }
// ***** Hash state
static void mc_hash_binary(mc_hash_t * hash, const void *s, size_t len)
{
- const char *p = (const void *) s;
- int i;
- for (i = 0; i != len; ++i) {
+ const char *p = (const char*) s;
+ for (size_t i = 0; i != len; ++i) {
MC_HASH(*hash, p[i]);
}
}
XBT_DEBUG("END hash %i", num_state);
return hash;
}
+
+}
#include "mc_protocol.h"
#include "mc_client.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc,
"Logging specific to MC ignore mechanism");
}
}
}
+
+}
#include "mc_smx.h"
#include "mc_client.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
"Logging specific to algorithms for liveness properties verification");
/* Traverse the stack backwards until a pair with a non empty interleave
set is found, deleting all the pairs that have it empty in the way. */
- while ((current_pair = xbt_fifo_shift(mc_stack)) != NULL) {
+ while ((current_pair = (mc_pair_t) xbt_fifo_shift(mc_stack)) != NULL) {
if (current_pair->requests > 0) {
/* We found a backtracking point */
XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
mmalloc_set_current_heap(heap);
}
+
+}
/* 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/misc.h>
+
#include "mc_object_info.h"
#include "mc_private.h"
+extern "C" {
+
/** Resolve snapshot in the process address space
*
* @param object Process address of the struct/class
else
return (void *) state.stack[state.stack_size - 1];
}
+
+}
#include "mc_object_info.h"
#include "mc_private.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory, mc,
"Logging specific to MC (memory)");
if (mc_heap && mc_heap != std_heap)
xbt_mheap_destroy(mc_heap);
}
+
+}
#ifndef MC_MMALLOC_H
#define MC_MMALLOC_H
+#include <xbt/misc.h>
#include <xbt/mmalloc.h>
/** file
* Normally the system should operate in std, for switching to raw mode
* you must wrap the code between MC_SET_RAW_MODE and MC_UNSET_RAW_MODE.
*/
-
+
+SG_BEGIN_DECL()
+
extern xbt_mheap_t std_heap;
extern xbt_mheap_t mc_heap;
#define MC_SET_MC_HEAP mmalloc_set_current_heap(mc_heap)
#define MC_SET_STD_HEAP mmalloc_set_current_heap(std_heap)
+SG_END_DECL()
+
#endif
#include "mc_model_checker.h"
#include "mc_page_store.h"
+extern "C" {
+
mc_model_checker_t mc_model_checker = NULL;
mc_model_checker_t MC_model_checker_new(pid_t pid, int socket)
&maxpid, sizeof(maxpid));
return maxpid;
}
+
+}
#include "mc_object_info.h"
#include "mc_private.h"
+extern "C" {
+
dw_frame_t MC_file_object_info_find_function(mc_object_info_t info, const void *ip)
{
xbt_dynar_t dynar = info->functions_index;
return NULL;
}
+
+}
// ***** Object info
-enum mc_object_info_flags {
- MC_OBJECT_INFO_NONE = 0,
- MC_OBJECT_INFO_EXECUTABLE = 1
-};
+/** Bit field of options */
+typedef int mc_object_info_flags;
+#define MC_OBJECT_INFO_NONE 0
+#define MC_OBJECT_INFO_EXECUTABLE 1
struct s_mc_object_info {
- enum mc_object_info_flags flags;
+ mc_object_info_flags flags;
char* file_name;
const void* start, *end;
char *start_exec, *end_exec; // Executable segment
#include "mc_mmu.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_page_snapshot, mc,
"Logging specific to mc_page_snapshot");
}
#endif /* SIMGRID_TEST */
+
+}
#include "mc_liveness.h"
#include "mc_private.h"
+extern "C" {
+
mc_pair_t MC_pair_new()
{
mc_pair_t p = NULL;
{
MC_pair_delete((mc_pair_t) * (void **) p);
}
+
+}
#include "mc_smx.h"
#include "mc_server.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
"MC process information");
}
static const s_mc_address_space_class_t mc_process_class = {
- .read = (void*) &MC_process_read,
- .get_process = (void*) MC_process_get_process
+ .read = (mc_address_space_class_read_callback_t) &MC_process_read,
+ .get_process = (mc_address_space_class_get_process_callback_t) MC_process_get_process
};
bool MC_is_process(mc_address_space_t p)
process->status = 0;
process->memory_map = MC_get_memory_map(pid);
process->memory_file = -1;
- process->cache_flags = 0;
+ process->cache_flags = MC_PROCESS_CACHE_FLAG_NONE;
process->heap = NULL;
process->heap_info = NULL;
MC_process_init_memory_map_info(process);
unw_destroy_addr_space(process->unw_addr_space);
process->unw_addr_space = NULL;
- process->cache_flags = 0;
+ process->cache_flags = MC_PROCESS_CACHE_FLAG_NONE;
free(process->heap);
process->heap = NULL;
// Read/dereference/refresh the std_heap pointer:
if (!process->heap) {
xbt_mheap_t oldheap = mmalloc_set_current_heap(mc_heap);
- process->heap = malloc(sizeof(struct mdesc));
+ process->heap = (struct mdesc*) malloc(sizeof(struct mdesc));
mmalloc_set_current_heap(oldheap);
}
MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
(process->heap->heaplimit + 1) * sizeof(malloc_info);
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
- process->heap_info = realloc(process->heap_info, malloc_info_bytesize);
+ process->heap_info = (malloc_info*) realloc(process->heap_info, malloc_info_bytesize);
mmalloc_set_current_heap(heap);
MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
const char* current_name = NULL;
- size_t i = 0;
- for (i=0; i < maps->mapsize; i++) {
+ for (ssize_t i=0; i < maps->mapsize; i++) {
map_region_t reg = &(maps->regions[i]);
const char* pathname = maps->regions[i].pathname;
regfree(&res.version_re);
// Resolve time (including accress differents objects):
- for (i=0; i!=process->object_infos_size; ++i)
+ for (size_t i=0; i!=process->object_infos_size; ++i)
MC_post_process_object_info(process, process->object_infos[i]);
xbt_assert(process->maestro_stack_start, "Did not find maestro_stack_start");
xbt_die("No simple location for this variable");
if (!var->type->full_type)
xbt_die("Partial type for %s, cannot check size", name);
- if (var->type->full_type->byte_size != size)
+ if ((size_t) var->type->full_type->byte_size != size)
xbt_die("Unexpected size for %s (expected %zi, was %zi)",
name, size, (size_t) var->type->full_type->byte_size);
- MC_process_read(process, MC_PROCESS_NO_FLAG, target, var->address, size,
+ MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE, target, var->address, size,
MC_PROCESS_INDEX_ANY);
}
if (MC_process_is_self(process))
return strdup((char*) address);
- size_t len = 128;
- char* res = malloc(len);
+ off_t len = 128;
+ char* res = (char*) malloc(len);
off_t off = 0;
while (1) {
off += c;
if (off == len) {
len *= 2;
- res = realloc(res, len);
+ res = (char*) realloc(res, len);
}
}
}
const size_t buffer_size = 30;
char buffer[buffer_size];
int res = snprintf(buffer, buffer_size, "/proc/%lli/mem", (long long) pid);
- if (res < 0 || res >= buffer_size) {
+ if (res < 0 || (size_t) res >= buffer_size) {
errno = ENAMETOOLONG;
return -1;
}
return real_count;
}
-const void* MC_process_read(mc_process_t process, e_adress_space_read_flags_t flags,
+const void* MC_process_read(mc_process_t process, adress_space_read_flags_t flags,
void* local, const void* remote, size_t len,
int process_index)
{
const void* MC_process_read_simple(mc_process_t process,
void* local, const void* remote, size_t len)
{
- e_adress_space_read_flags_t flags = MC_PROCESS_NO_FLAG;
+ adress_space_read_flags_t flags = MC_ADDRESS_SPACE_READ_FLAGS_NONE;
int index = MC_PROCESS_INDEX_ANY;
MC_process_read(process, flags, local, remote, len, index);
return local;
}
}
-void MC_simcall_handle(smx_simcall_t req, int value)
-{
- if (MC_process_is_self(&mc_model_checker->process)) {
- SIMIX_simcall_handle(req, value);
- return;
- }
-
- unsigned i;
- mc_smx_process_info_t pi = NULL;
-
- xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
- if (req == &pi->copy.simcall) {
- MC_server_simcall_handle(&mc_model_checker->process, pi->copy.pid, value);
- return;
- }
- }
-
- xbt_die("Could not find the request");
}
int MC_process_vm_open(pid_t pid, int flags);
-typedef enum {
- MC_PROCESS_NO_FLAG = 0,
- MC_PROCESS_SELF_FLAG = 1,
-} e_mc_process_flags_t;
+typedef int mc_process_flags_t;
+#define MC_PROCESS_NO_FLAG 0
+#define MC_PROCESS_SELF_FLAG 1
// Those flags are used to track down which cached information
// is still up to date and which information needs to be updated.
-typedef enum {
- MC_PROCESS_CACHE_FLAG_HEAP = 1,
- MC_PROCESS_CACHE_FLAG_MALLOC_INFO = 2,
- MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES = 4,
-} e_mc_process_cache_flags_t ;
+typedef int mc_process_cache_flags_t;
+#define MC_PROCESS_CACHE_FLAG_NONE 0
+#define MC_PROCESS_CACHE_FLAG_HEAP 1
+#define MC_PROCESS_CACHE_FLAG_MALLOC_INFO 2
+#define MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES 4
typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_info_t;
*/
struct s_mc_process {
s_mc_address_space_t address_space;
- e_mc_process_flags_t process_flags;
+ mc_process_flags_t process_flags;
pid_t pid;
int socket;
int status;
xbt_dynar_t smx_old_process_infos;
/** State of the cache (which variables are up to date) */
- e_mc_process_cache_flags_t cache_flags;
+ mc_process_cache_flags_t cache_flags;
/** Address of the heap structure in the MCed process. */
void* heap_address;
* @param len data size
*/
const void* MC_process_read(mc_process_t process,
- e_adress_space_read_flags_t flags,
+ adress_space_read_flags_t flags,
void* local, const void* remote, size_t len,
int process_index);
#include "mc_protocol.h"
#include "mc_client.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_protocol, mc, "Generic MC protocol logic");
int MC_protocol_send(int socket, void* message, size_t size)
return 0;
}
-int MC_protocol_send_simple_message(int socket, int type)
+int MC_protocol_send_simple_message(int socket, e_mc_message_type type)
{
s_mc_message_t message;
message.type = type;
s_mc_message_t message;
message.type = MC_MESSAGE_NONE;
- size_t s;
+ ssize_t s;
while ((s = MC_receive_message(socket, &message, sizeof(message), 0)) == -1) {
if (errno == EINTR)
continue;
return 2;
}
}
- if (s < sizeof(message) || message.type != MC_MESSAGE_HELLO) {
+ if ((size_t) s < sizeof(message) || message.type != MC_MESSAGE_HELLO) {
XBT_ERROR("Did not receive suitable HELLO message. Who are you?");
return 3;
}
return "?";
}
}
+
+}
} s_mc_register_symbol_message_t, * mc_register_symbol_message_t;
int MC_protocol_send(int socket, void* message, size_t size);
-int MC_protocol_send_simple_message(int socket, int type);
+int MC_protocol_send_simple_message(int socket, e_mc_message_type type);
int MC_protocol_hello(int socket);
ssize_t MC_receive_message(int socket, void* message, size_t size, int options);
#include "mc_smx.h"
#endif
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc,
" Logging specific to MC record/replay facility");
xbt_dynar_push(dynar, &item);
// Find next chunk:
- char* end = strchr(current, ';');
+ const char* end = strchr(current, ';');
if(end==NULL)
break;
else
{
mc_time = xbt_new0(double, simix_process_maxpid);
}
+
+}
#include "mc_private.h"
#include "mc_smx.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
"Logging specific to MC (request)");
// Those are internal requests, we do not need indirection
// because those objects are copies:
- smx_synchro_t synchro1, synchro2;
+ smx_synchro_t synchro1 = NULL, synchro2 = NULL;
if (r1->call == SIMCALL_COMM_WAIT) {
synchro1 = simcall_comm_wait__get__comm(r1);
}
char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t request_type)
{
- bool use_remote_comm;
+ bool use_remote_comm = false;
switch(request_type) {
case MC_REQUEST_SIMIX:
use_remote_comm = true;
// Get the element:
smx_synchro_t remote_action;
- memcpy(buffer + comms.elmsize * cursor, &remote_action, sizeof(remote_action));
+ memcpy(&remote_action, buffer + comms.elmsize * cursor, sizeof(remote_action));
// Dereference the pointer:
s_smx_synchro_t action;
return str;
}
+
+}
#include "xbt/mmalloc/mmprivate.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
"Logging specific to MC safety verification ");
executed before it. If it does then add it to the interleave set of the
state that executed that previous request. */
- while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
+ while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
if (mc_reduce_kind == e_mc_reduce_dpor) {
req = MC_state_get_internal_request(state);
const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
xbt_abort();
//MC_exit();
}
+
+}
#include "mc_private.h"
#include "mc_ignore.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
// HArdcoded index for now:
int res = MC_protocol_send_simple_message(socket, MC_MESSAGE_CONTINUE);
if (res)
throw std::system_error(res, std::system_category());
- process->cache_flags = (e_mc_process_cache_flags_t) 0;
+ process->cache_flags = (mc_process_cache_flags_t) 0;
}
static
m.pid = pid;
m.value = value;
MC_protocol_send(mc_model_checker->process.socket, &m, sizeof(m));
- process->cache_flags = (e_mc_process_cache_flags_t) 0;
+ process->cache_flags = (mc_process_cache_flags_t) 0;
while (mc_model_checker->process.running) {
if (!mc_server->handle_events())
return;
{
server->loop();
}
+
+}
#ifndef MC_SERVER_H
#define MC_SERVER_H
+#include <poll.h>
+
#include <stdint.h>
#include <stdbool.h>
#include "mc_smx.h"
#include "mc_model_checker.h"
+extern "C" {
+
static
void MC_smx_process_info_clear(mc_smx_process_info_t p)
{
// Load each element of the dynar from the MCed process:
int i = 0;
- for (p = swag.head; p; ++i) {
+ for (p = (smx_process_t) swag.head; p; ++i) {
s_mc_smx_process_info_t info;
info.address = p;
xbt_dynar_push(target, &info);
// Lookup next process address:
- p = xbt_swag_getNext(&info.copy, swag.offset);
+ p = (smx_process_t) xbt_swag_getNext(&info.copy, swag.offset);
}
assert(i == swag.count);
}
return res;
}
}
+
+}
#include "mc_mmu.h"
#include "mc_page_store.h"
+extern "C" {
+
/** @brief Find the snapshoted region from a pointer
*
* @param addr Pointer
if (process_index < 0) {
xbt_die("Missing process index");
}
- if (process_index >= region->privatized.regions_count) {
+ if (process_index >= (int) region->privatized.regions_count) {
xbt_die("Invalid process index");
}
mc_mem_region_t priv_region = region->privatized.regions[process_index];
* @return Pointer where the data is located (target buffer or original location)
*/
const void* MC_snapshot_read(
- mc_snapshot_t snapshot, e_adress_space_read_flags_t flags,
+ mc_snapshot_t snapshot, adress_space_read_flags_t flags,
void* target, const void* addr, size_t size, int process_index)
{
mc_mem_region_t region = mc_get_snapshot_region(addr, snapshot, process_index);
#include "mc/mc_snapshot.h"
#include "mc/mc_mmu.h"
+extern "C" {
+
XBT_TEST_SUITE("mc_snapshot", "Snapshots");
static inline void init_memory(void* mem, size_t size)
{
char* dest = (char*) mem;
- for (int i=0; i!=size; ++i) {
+ for (size_t i = 0; i < size; ++i) {
dest[i] = rand() & 255;
}
}
mc_model_checker = NULL;
}
+}
+
#endif /* SIMGRID_TEST */
+
+}
const void* MC_region_read_fragmented(mc_mem_region_t region, void* target, const void* addr, size_t size);
-const void* MC_snapshot_read(mc_snapshot_t snapshot, e_adress_space_read_flags_t flags,
+const void* MC_snapshot_read(mc_snapshot_t snapshot, adress_space_read_flags_t flags,
void* target, const void* addr, size_t size, int process_index);
int MC_snapshot_region_memcmp(
const void* addr1, mc_mem_region_t region1,
#include "mc_comm_pattern.h"
#include "mc_smx.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc,
"Logging specific to MC (state)");
simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
break;
- case SIMCALL_MC_RANDOM:
+ case SIMCALL_MC_RANDOM: {
state->internal_req = *req;
int random_max = simcall_mc_random__get__max(req);
if (value != random_max) {
);
}
break;
+ }
default:
state->internal_req = *req;
return NULL;
}
+
+}
*/
// We need this for the register indices:
-#define _GNU_SOURCE
+// #define _GNU_SOURCE
#include <string.h>
#include "mc_process.h"
#include "mc_unw.h"
+extern "C" {
+
// ***** Implementation
/** Get frame unwind information (libunwind method)
{
mc_unw_context_t context = (mc_unw_context_t) arg;
if (write)
- return -UNW_EREADONLYREG;
+ return - UNW_EREADONLYREG;
MC_address_space_read(context->address_space,
- 0, valp, (void*) addr, sizeof(unw_word_t), MC_PROCESS_INDEX_ANY);
+ MC_ADDRESS_SPACE_READ_FLAGS_NONE, valp, (void*) addr, sizeof(unw_word_t), MC_PROCESS_INDEX_ANY);
// We don't handle failure gracefully.
return 0;
}
unw_context_t* context = &as_context->context;
if (write)
return -UNW_EREADONLYREG;
- greg_t* preg = get_reg(context, regnum);
+ greg_t* preg = (greg_t*) get_reg(context, regnum);
if (!preg)
return -UNW_EBADREG;
*valp = *preg;
return unw_init_remote(cursor, context->process->unw_addr_space, context);
}
+
+}
-#define _GNU_SOURCE
-
#include <sys/types.h>
#include <sys/uio.h>
#include "mc_unw.h"
+extern "C" {
+
/** \file
* Libunwind namespace implementation using process_vm_readv.
*.
static inline
pid_t _UPT_getpid(void* arg)
{
- struct _UPT_info* info = arg;
+ struct _UPT_info* info = (_UPT_info*) arg;
return info->pid;
}
struct iovec remote = { (void*) addr, size };
s = process_vm_readv(pid, &local, 1, &remote, 1, 0);
if (s >= 0) {
- if (s != size)
+ if ((size_t) s != size)
return - UNW_EINVAL;
else
return 0;
.resume = &_UPT_resume,
.get_proc_name = &_UPT_get_proc_name
};
+
+}
#include "mc_process.h"
#include "mc_smx.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
"Logging specific to state equaity detection mechanisms");
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
- int cursor = 0, previous_cursor, next_cursor;
+ int cursor = 0, previous_cursor;
int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
void *ref_test;
*min = previous_cursor;
previous_cursor--;
}
- next_cursor = cursor + 1;
+ size_t next_cursor = cursor + 1;
while (next_cursor < xbt_dynar_length(list)) {
if (_sg_mc_liveness) {
ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
communications are not finished (at least, data are transfered). These communications
are incomplete and they cannot be analyzed and compared with the initial pattern. */
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- int current_process = 1;
+ size_t current_process = 1;
while (current_process < MC_smx_get_maxpid()) {
if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
}
// We have reached the maximum number of stored states;
- if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
+ if ((ssize_t) xbt_dynar_length(visited_states) > _sg_mc_visited) {
XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
}
}
- if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
+ if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
int min2 = mc_stats->expanded_pairs;
unsigned int cursor2 = 0;
unsigned int index2 = 0;
mmalloc_set_current_heap(heap);
return -1;
}
+
+}
#include "mc_memory_map.h"
#include "mc_private.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory_map, mc,
"Logging specific to algorithms for memory_map");
/* parsed stuff from the temporal memreg variable */
XBT_DEBUG("Found region for %s",
memreg.pathname ? memreg.pathname : "(null)");
- ret->regions =
+ ret->regions = (map_region_t)
xbt_realloc(ret->regions, sizeof(memreg) * (ret->mapsize + 1));
memcpy(ret->regions + ret->mapsize, &memreg, sizeof(memreg));
ret->mapsize++;
xbt_free(map->regions);
xbt_free(map);
}
+
+}
sysv_maestro_context = context;
}
+#ifdef HAVE_MC
if (MC_is_active() && code) {
MC_new_stack_area(context->stack, ((smx_context_t)context)->process,
&(context->uc), smx_context_usable_stack_size);
}
+#endif
return (smx_context_t) context;
}
#ifndef __MMPRIVATE_H
#define __MMPRIVATE_H 1
+#include <xbt/misc.h>
+
#include "portable.h"
#include "xbt/xbt_os_thread.h"
#include "xbt/mmalloc.h"
#define ADDRESS(B) ((void*) (((ADDR2UINT(B)) - 1) * BLOCKSIZE + (char*) mdp -> heapbase))
+SG_BEGIN_DECL()
+
/* Doubly linked lists of free fragments. */
struct list {
struct list *next;
size_t mmalloc_get_bytes_used_remote(size_t heaplimit, const malloc_info* heapinfo);
+SG_END_DECL()
+
#endif /* __MMPRIVATE_H */