set(MC_SRC
src/mc/mc_forward.h
+ src/mc/mc_process.h
+ src/mc/mc_process.c
src/mc/mc_mmalloc.h
src/mc/mc_model_checker.h
src/mc/mc_object_info.h
+ src/mc/mc_object_info.c
src/mc/mc_checkpoint.c
src/mc/mc_snapshot.h
src/mc/mc_snapshot.c
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/running_power' to '1e9'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check communication determinism
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> [0.000000] [mc_comm_determinism/INFO] The communications pattern of the process 1 is different! (Different communication : 1)
> [0.000000] [mc_comm_determinism/INFO] ****************************************************
> [0.000000] [mc_comm_determinism/INFO] ***** Non-deterministic communications pattern *****
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/running_power' to '1e9'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check communication determinism
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> [0.000000] [mc_global/INFO] Expanded states = 520
> [0.000000] [mc_global/INFO] Visited states = 1476
> [0.000000] [mc_global/INFO] Executed transitions = 1312
extern xbt_dynar_t mc_heap_comparison_ignore;
extern xbt_dynar_t stacks_areas;
-extern void *maestro_stack_start;
-extern void *maestro_stack_end;
/********************************* Global *************************************/
void _mc_cfg_cb_reduce(const char *name, int pos);
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
"Logging specific to mc_checkpoint");
-char *libsimgrid_path;
-
/************************************ Free functions **************************************/
/*****************************************************************************************/
static void MC_get_memory_regions(mc_snapshot_t snapshot)
{
+ mc_process_t process = &mc_model_checker->process;
void *start_heap = std_heap->base;
void *end_heap = std_heap->breakval;
snapshot->privatization_regions = NULL;
MC_snapshot_add_region(snapshot, 1,
- mc_libsimgrid_info->start_rw, mc_libsimgrid_info->start_rw,
- mc_libsimgrid_info->end_rw - mc_libsimgrid_info->start_rw);
+ process->libsimgrid_info->start_rw, process->libsimgrid_info->start_rw,
+ process->libsimgrid_info->end_rw - process->libsimgrid_info->start_rw);
#ifdef HAVE_SMPI
size_t i;
mc_mem_region_t ref_reg =
mc_model_checker->parent_snapshot ? mc_model_checker->parent_snapshot->privatization_regions[i] : NULL;
snapshot->privatization_regions[i] =
- MC_region_new(-1, mc_binary_info->start_rw, smpi_privatisation_regions[i].address, size_data_exe, ref_reg);
+ MC_region_new(-1, process->binary_info->start_rw, smpi_privatisation_regions[i].address, size_data_exe, ref_reg);
}
snapshot->privatization_index = smpi_loaded_page;
snapshot->regions[2] = NULL;
#endif
{
MC_snapshot_add_region(snapshot, 2,
- mc_binary_info->start_rw, mc_binary_info->start_rw,
- mc_binary_info->end_rw - mc_binary_info->start_rw);
+ process->binary_info->start_rw, process->binary_info->start_rw,
+ process->binary_info->end_rw - process->binary_info->start_rw);
snapshot->privatization_regions = NULL;
snapshot->privatization_index = -1;
}
}
-/** @brief Finds the range of the different memory segments and binary paths */
-void MC_init_memory_map_info()
-{
-
- unsigned int i = 0;
- s_map_region_t reg;
- memory_map_t maps = MC_get_memory_map();
-
- maestro_stack_start = NULL;
- maestro_stack_end = NULL;
- libsimgrid_path = NULL;
-
- while (i < maps->mapsize) {
- reg = maps->regions[i];
- if (maps->regions[i].pathname == NULL) {
- // Nothing to do
- } else if ((reg.prot & PROT_WRITE)
- && !memcmp(maps->regions[i].pathname, "[stack]", 7)) {
- maestro_stack_start = reg.start_addr;
- maestro_stack_end = reg.end_addr;
- } else if ((reg.prot & PROT_READ) && (reg.prot & PROT_EXEC)
- && !memcmp(basename(maps->regions[i].pathname), "libsimgrid",
- 10)) {
- if (libsimgrid_path == NULL)
- libsimgrid_path = strdup(maps->regions[i].pathname);
- }
- i++;
- }
-
- xbt_assert(maestro_stack_start, "maestro_stack_start");
- xbt_assert(maestro_stack_end, "maestro_stack_end");
- xbt_assert(libsimgrid_path, "libsimgrid_path&");
-
- MC_free_memory_map(maps);
-
-}
-
/** \brief Fills the position of the segments (executable, read-only, read/write).
*
* TODO, use dl_iterate_phdr to be more robust
static void mc_fill_local_variables_values(mc_stack_frame_t stack_frame,
dw_frame_t scope, int process_index, xbt_dynar_t result)
{
+ mc_process_t process = &mc_model_checker->process;
+
void *ip = (void *) stack_frame->ip;
if (ip < scope->low_pc || ip >= scope->high_pc)
return;
continue;
int region_type;
- if ((long) stack_frame->ip > (long) mc_libsimgrid_info->start_exec)
+ if ((long) stack_frame->ip > (long) process->libsimgrid_info->start_exec)
region_type = 1;
else
region_type = 2;
static xbt_dynar_t MC_unwind_stack_frames(void *stack_context)
{
+ mc_process_t process = &mc_model_checker->process;
xbt_dynar_t result =
xbt_dynar_new(sizeof(mc_stack_frame_t), MC_stack_frame_free_voipd);
// TODO, use real addresses in frame_t instead of fixing it here
- dw_frame_t frame = MC_find_function_by_ip((void *) ip);
+ dw_frame_t frame = MC_process_find_function(process, (void *) ip);
stack_frame->frame = frame;
if (frame) {
int snapshot_compare(void *state1, void *state2)
{
+ mc_process_t process = &mc_model_checker->process;
mc_snapshot_t s1, s2;
int num1, num2;
};
#endif
- mc_object_info_t object_infos[] = { NULL, mc_libsimgrid_info, mc_binary_info };
+ mc_object_info_t object_infos[] = { NULL, process->libsimgrid_info, process->binary_info };
int k = 0;
for (k = 2; k != 0; --k) {
/* Compare global variables */
#ifdef HAVE_SMPI
- if (object_infos[k] == mc_binary_info && smpi_privatize_global_variables) {
+ if (object_infos[k] == process->binary_info && smpi_privatize_global_variables) {
// Compare the global variables separately for each simulates process:
for (int process_index = 0; process_index < smpi_process_count(); process_index++) {
is_diff =
xbt_dynar_t mc_heap_comparison_ignore;
xbt_dynar_t stacks_areas;
-void *maestro_stack_start, *maestro_stack_end;
+
/********************************* Backtrace ***********************************/
xbt_dynar_t previous, int size,
int check_ignore)
{
+ mc_process_t process = &mc_model_checker->process;
int i = 0;
void *addr_pointed1, *addr_pointed2;
addr_pointed1 = mc_snapshot_read_pointer((char *) real_area1 + pointer_align, snapshot1, process_index);
addr_pointed2 = mc_snapshot_read_pointer((char *) real_area2 + pointer_align, snapshot2, process_index);
- if (addr_pointed1 > maestro_stack_start
- && addr_pointed1 < maestro_stack_end
- && addr_pointed2 > maestro_stack_start
- && addr_pointed2 < maestro_stack_end) {
+ if (addr_pointed1 > process->maestro_stack_start
+ && addr_pointed1 < process->maestro_stack_end
+ && addr_pointed2 > process->maestro_stack_start
+ && addr_pointed2 < process->maestro_stack_end) {
i = pointer_align + sizeof(void *);
continue;
} else if (addr_pointed1 > state->s_heap
info->functions_index = index;
}
-mc_object_info_t MC_ip_find_object_info(void *ip)
-{
- size_t i;
- for (i = 0; i != mc_object_infos_size; ++i) {
- if (ip >= (void *) mc_object_infos[i]->start_exec
- && ip <= (void *) mc_object_infos[i]->end_exec) {
- return mc_object_infos[i];
- }
- }
- return NULL;
-}
-
-static dw_frame_t MC_find_function_by_ip_and_object(void *ip,
- mc_object_info_t info)
-{
- xbt_dynar_t dynar = info->functions_index;
- mc_function_index_item_t base =
- (mc_function_index_item_t) xbt_dynar_get_ptr(dynar, 0);
- int i = 0;
- int j = xbt_dynar_length(dynar) - 1;
- while (j >= i) {
- int k = i + ((j - i) / 2);
- if (ip < base[k].low_pc) {
- j = k - 1;
- } else if (ip >= base[k].high_pc) {
- i = k + 1;
- } else {
- return base[k].function;
- }
- }
- return NULL;
-}
-
-dw_frame_t MC_find_function_by_ip(void *ip)
-{
- mc_object_info_t info = MC_ip_find_object_info(ip);
- if (info == NULL)
- return NULL;
- else
- return MC_find_function_by_ip_and_object(ip, info);
-}
-
static void MC_post_process_variables(mc_object_info_t info)
{
unsigned cursor = 0;
MC_dwarf_register_non_global_variable(info, frame, variable);
}
-void MC_post_process_object_info(mc_object_info_t info)
+void MC_post_process_object_info(mc_process_t process, mc_object_info_t info)
{
xbt_dict_cursor_t cursor = NULL;
char *key = NULL;
// Resolve full_type:
if (type->name && type->byte_size == 0) {
- for (size_t i = 0; i != mc_object_infos_size; ++i) {
+ for (size_t i = 0; i != process->object_infos_size; ++i) {
dw_type_t same_type =
- xbt_dict_get_or_null(mc_object_infos[i]->full_types_by_name,
+ xbt_dict_get_or_null(process->object_infos[i]->full_types_by_name,
type->name);
if (same_type && same_type->name && same_type->byte_size) {
type->full_type = same_type;
typedef struct s_mc_pages_store s_mc_pages_store_t, *mc_pages_store_t;
typedef struct s_mc_snapshot s_mc_snapshot_t, *mc_snapshot_t;
+typedef struct s_mc_process s_mc_process_t, * mc_process_t;
typedef struct s_mc_model_checker s_mc_model_checker_t, *mc_model_checker_t;
extern mc_model_checker_t mc_model_checker;
#ifndef _XBT_WIN32
#include <unistd.h>
-#include <sys/types.h>
#include <sys/wait.h>
#include <sys/time.h>
-#include <sys/mman.h>
-#include <libgen.h>
#endif
#include "simgrid/sg_config.h"
/* Liveness */
xbt_automaton_t _mc_property_automaton = NULL;
-/* Variables */
-mc_object_info_t mc_libsimgrid_info = NULL;
-mc_object_info_t mc_binary_info = NULL;
-
-mc_object_info_t mc_object_infos[2] = { NULL, NULL };
-
-size_t mc_object_infos_size = 2;
-
/* Dot output */
FILE *dot_output = NULL;
const char *colors[13];
}
-static void MC_init_debug_info(void)
-{
- XBT_INFO("Get debug information ...");
-
- memory_map_t maps = MC_get_memory_map();
-
- /* Get local variables for state equality detection */
- mc_binary_info = MC_find_object_info(maps, xbt_binary_name, 1);
- mc_object_infos[0] = mc_binary_info;
-
- mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path, 0);
- mc_object_infos[1] = mc_libsimgrid_info;
-
- // Use information of the other objects:
- MC_post_process_object_info(mc_binary_info);
- MC_post_process_object_info(mc_libsimgrid_info);
-
- MC_free_memory_map(maps);
- XBT_INFO("Get debug information done !");
-}
-
-
mc_model_checker_t mc_model_checker = NULL;
mc_model_checker_t MC_model_checker_new()
mc->pages = mc_pages_store_new();
mc->fd_clear_refs = -1;
mc->fd_pagemap = -1;
+ MC_process_init(&mc->process, getpid());
return mc;
}
mc_pages_store_delete(mc->pages);
if(mc->record)
xbt_dynar_free(&mc->record);
+ MC_process_clear(&mc->process);
}
void MC_init()
mc_stats = xbt_new0(s_mc_stats_t, 1);
mc_stats->state_size = 1;
- MC_init_memory_map_info();
- MC_init_debug_info(); /* FIXME : get debug information only if liveness verification or visited state reduction */
-
if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0'))
MC_init_dot_output();
mc_address_add(state->handled_addresses, pointed);
// Anything outside the R/W segments and the heap is not hashed:
- bool valid_pointer = (pointed >= (void *) mc_binary_info->start_rw
- && pointed <= (void *) mc_binary_info->end_rw)
- || (pointed >= (void *) mc_libsimgrid_info->start_rw
- && pointed <= (void *) mc_libsimgrid_info->end_rw)
+ bool valid_pointer = (pointed >= (void *) binary_info->start_rw
+ && pointed <= (void *) binary_info->end_rw)
+ || (pointed >= (void *) libsimgrid_info->start_rw
+ && pointed <= (void *) libsimgrid_info->end_rw)
|| (pointed >= std_heap
&& pointed < (void *) ((const char *) std_heap + STD_HEAP_SIZE));
if (!valid_pointer) {
}
const char *address = variable->address;
- bool valid_pointer = (address >= mc_binary_info->start_rw
- && address <= mc_binary_info->end_rw)
- || (address >= mc_libsimgrid_info->start_rw
- && address <= mc_libsimgrid_info->end_rw)
+ bool valid_pointer = (address >= binary_info->start_rw
+ && address <= binary_info->end_rw)
+ || (address >= libsimgrid_info->start_rw
+ && address <= libsimgrid_info->end_rw)
|| (address >= (const char *) std_heap
&& address < (const char *) std_heap + STD_HEAP_SIZE);
if (!valid_pointer)
MC_HASH(*hash, stack_frame->ip);
mc_object_info_t info;
- if (stack_frame->ip >= (unw_word_t) mc_libsimgrid_info->start_exec
- && stack_frame->ip < (unw_word_t) mc_libsimgrid_info->end_exec)
- info = mc_libsimgrid_info;
- else if (stack_frame->ip >= (unw_word_t) mc_binary_info->start_exec
- && stack_frame->ip < (unw_word_t) mc_binary_info->end_exec)
- info = mc_binary_info;
+ if (stack_frame->ip >= (unw_word_t) libsimgrid_info->start_exec
+ && stack_frame->ip < (unw_word_t) libsimgrid_info->end_exec)
+ info = libsimgrid_info;
+ else if (stack_frame->ip >= (unw_word_t) binary_info->start_exec
+ && stack_frame->ip < (unw_word_t) binary_info->end_exec)
+ info = binary_info;
else
continue;
mc_hash_t hash = MC_HASH_INIT;
MC_HASH(hash, xbt_swag_size(simix_global->process_list)); // process count
- // mc_hash_object_globals(&hash, &state, mc_binary_info);
- // mc_hash_object_globals(&hash, &state, mc_libsimgrid_info);
+ // mc_hash_object_globals(&hash, &state, binary_info);
+ // mc_hash_object_globals(&hash, &state, libsimgrid_info);
// mc_hash_stacks(&hash, &state, stacks);
mc_hash_state_destroy(&state);
void MC_ignore_global_variable(const char *name)
{
-
+ mc_process_t process = &mc_model_checker->process;
int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
MC_SET_MC_HEAP;
- xbt_assert(mc_libsimgrid_info, "MC subsystem not initialized");
+ xbt_assert(process->libsimgrid_info, "MC subsystem not initialized");
unsigned int cursor = 0;
dw_variable_t current_var;
int start = 0;
- int end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
+ int end = xbt_dynar_length(process->libsimgrid_info->global_variables) - 1;
while (start <= end) {
cursor = (start + end) / 2;
current_var =
- (dw_variable_t) xbt_dynar_get_as(mc_libsimgrid_info->global_variables,
+ (dw_variable_t) xbt_dynar_get_as(process->libsimgrid_info->global_variables,
cursor, dw_variable_t);
if (strcmp(current_var->name, name) == 0) {
- xbt_dynar_remove_at(mc_libsimgrid_info->global_variables, cursor, NULL);
+ xbt_dynar_remove_at(process->libsimgrid_info->global_variables, cursor, NULL);
start = 0;
- end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
+ end = xbt_dynar_length(process->libsimgrid_info->global_variables) - 1;
} else if (strcmp(current_var->name, name) < 0) {
start = cursor + 1;
} else {
void MC_ignore_local_variable(const char *var_name, const char *frame_name)
{
+ mc_process_t process = &mc_model_checker->process;
+
int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
MC_SET_MC_HEAP;
- MC_ignore_local_variable_in_object(var_name, frame_name, mc_libsimgrid_info);
+ MC_ignore_local_variable_in_object(var_name, frame_name, process->libsimgrid_info);
if (frame_name != NULL)
- MC_ignore_local_variable_in_object(var_name, frame_name, mc_binary_info);
+ MC_ignore_local_variable_in_object(var_name, frame_name, process->binary_info);
if (!raw_mem_set)
MC_SET_STD_HEAP;
#include "xbt_modinter.h"
void MC_memory_exit(void)
{
- MC_free_object_info(&mc_binary_info);
- MC_free_object_info(&mc_libsimgrid_info);
-
if (mc_heap)
xbt_mheap_destroy(mc_heap);
}
#ifndef MC_MEMORY_MAP_H
#define MC_MEMORY_MAP_H
+#include <sys/types.h>
+
#include <simgrid_config.h>
#include "mc_forward.h"
};
-void MC_init_memory_map_info(void);
-memory_map_t MC_get_memory_map(void);
+memory_map_t MC_get_memory_map(pid_t pid);
void MC_free_memory_map(memory_map_t map);
SG_END_DECL()
#include <simgrid_config.h>
#include "mc_forward.h"
+#include "mc_process.h"
SG_BEGIN_DECL()
int fd_clear_refs;
int fd_pagemap;
xbt_dynar_t record;
+ s_mc_process_t process;
};
mc_model_checker_t MC_model_checker_new(void);
--- /dev/null
+#include <stddef.h>
+
+#include <xbt/dynar.h>
+
+#include "mc_object_info.h"
+#include "mc_private.h"
+
+dw_frame_t MC_file_object_info_find_function(mc_object_info_t info, void *ip)
+{
+ xbt_dynar_t dynar = info->functions_index;
+ mc_function_index_item_t base =
+ (mc_function_index_item_t) xbt_dynar_get_ptr(dynar, 0);
+ int i = 0;
+ int j = xbt_dynar_length(dynar) - 1;
+ while (j >= i) {
+ int k = i + ((j - i) / 2);
+ if (ip < base[k].low_pc) {
+ j = k - 1;
+ } else if (ip >= base[k].high_pc) {
+ i = k + 1;
+ } else {
+ return base[k].function;
+ }
+ }
+ return NULL;
+}
-/* Copyright (c) 2007-2014. The SimGrid Team.
+ /* Copyright (c) 2007-2014. The SimGrid Team.
* All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
#include "mc_forward.h"
#include "mc_location.h"
+#include "mc_process.h"
SG_BEGIN_DECL();
mc_object_info_t MC_find_object_info(memory_map_t maps, char* name, int executable);
void MC_free_object_info(mc_object_info_t* p);
-void MC_post_process_object_info(mc_object_info_t info);
+dw_frame_t MC_file_object_info_find_function(mc_object_info_t info, void *ip);
+
+void MC_post_process_object_info(mc_process_t process, mc_object_info_t info);
void MC_dwarf_get_variables(mc_object_info_t info);
void MC_dwarf_get_variables_libdw(mc_object_info_t info);
// Not used:
char* get_type_description(mc_object_info_t info, char *type_name);
-extern mc_object_info_t mc_libsimgrid_info;
-extern mc_object_info_t mc_binary_info;
-extern mc_object_info_t mc_object_infos[2];
-extern size_t mc_object_infos_size;
-
void* mc_member_resolve(const void* base, dw_type_t type, dw_type_t member, mc_snapshot_t snapshot, int process_index);
struct s_dw_variable{
void MC_print_statistics(mc_stats_t stats);
-extern char *libsimgrid_path;
-
/********************************** Snapshot comparison **********************************/
typedef struct s_mc_comparison_times{
/********************************** Variables with DWARF **********************************/
-dw_frame_t MC_find_function_by_ip(void* ip);
-mc_object_info_t MC_ip_find_object_info(void* ip);
-
void MC_find_object_address(memory_map_t maps, mc_object_info_t result);
/********************************** Miscellaneous **********************************/
--- /dev/null
+#include <stddef.h>
+
+#include <sys/types.h>
+#include <unistd.h>
+#include <sys/mman.h> // PROT_*
+
+#include <libgen.h>
+
+#include "mc_process.h"
+#include "mc_object_info.h"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
+ "MC process information");
+
+static void MC_init_memory_map_info(mc_process_t process);
+static void MC_init_debug_info(mc_process_t process);
+
+void MC_process_init(mc_process_t process, pid_t pid)
+{
+ process->process_flags = MC_PROCESS_NO_FLAG;
+ process->pid = pid;
+ if (pid==getpid())
+ process->process_flags |= MC_PROCESS_SELF_FLAG;
+ process->memory_map = MC_get_memory_map(pid);
+ MC_init_memory_map_info(process);
+ MC_init_debug_info(process);
+}
+
+void MC_process_clear(mc_process_t process)
+{
+ process->process_flags = MC_PROCESS_NO_FLAG;
+ process->pid = 0;
+ MC_free_memory_map(process->memory_map);
+ process->memory_map = NULL;
+ process->maestro_stack_start = NULL;
+ process->maestro_stack_end = NULL;
+ free(process->libsimgrid_path);
+ process->libsimgrid_path = NULL;
+ MC_free_object_info(&process->binary_info);
+ MC_free_object_info(&process->libsimgrid_info);
+}
+
+/** @brief Finds the range of the different memory segments and binary paths */
+static void MC_init_memory_map_info(mc_process_t process)
+{
+ process->maestro_stack_start = NULL;
+ process->maestro_stack_end = NULL;
+ process->libsimgrid_path = NULL;
+
+ memory_map_t maps = process->memory_map;
+
+ unsigned int i = 0;
+ while (i < maps->mapsize) {
+ map_region_t reg = &(maps->regions[i]);
+ if (maps->regions[i].pathname == NULL) {
+ // Nothing to do
+ } else if ((reg->prot & PROT_WRITE)
+ && !memcmp(maps->regions[i].pathname, "[stack]", 7)) {
+ process->maestro_stack_start = reg->start_addr;
+ process->maestro_stack_end = reg->end_addr;
+ } else if ((reg->prot & PROT_READ) && (reg->prot & PROT_EXEC)
+ && !memcmp(basename(maps->regions[i].pathname), "libsimgrid",
+ 10)) {
+ if (process->libsimgrid_path == NULL)
+ process->libsimgrid_path = strdup(maps->regions[i].pathname);
+ }
+ i++;
+ }
+
+ xbt_assert(process->maestro_stack_start, "maestro_stack_start");
+ xbt_assert(process->maestro_stack_end, "maestro_stack_end");
+ xbt_assert(process->libsimgrid_path, "libsimgrid_path&");
+}
+
+static void MC_init_debug_info(mc_process_t process)
+{
+ XBT_INFO("Get debug information ...");
+
+ memory_map_t maps = process->memory_map;
+
+ // TODO, fix binary name
+
+ /* Get local variables for state equality detection */
+ process->binary_info = MC_find_object_info(maps, xbt_binary_name, 1);
+ process->object_infos[0] = process->binary_info;
+
+ process->libsimgrid_info = MC_find_object_info(maps, process->libsimgrid_path, 0);
+ process->object_infos[1] = process->libsimgrid_info;
+
+ process->object_infos_size = 2;
+
+ // Use information of the other objects:
+ MC_post_process_object_info(process, process->libsimgrid_info);
+ MC_post_process_object_info(process, process->binary_info);
+
+ XBT_INFO("Get debug information done !");
+}
+
+mc_object_info_t MC_process_find_object_info(mc_process_t process, void *ip)
+{
+ size_t i;
+ for (i = 0; i != process->object_infos_size; ++i) {
+ if (ip >= (void *) process->object_infos[i]->start_exec
+ && ip <= (void *) process->object_infos[i]->end_exec) {
+ return process->object_infos[i];
+ }
+ }
+ return NULL;
+}
+
+dw_frame_t MC_process_find_function(mc_process_t process, void *ip)
+{
+ mc_object_info_t info = MC_process_find_object_info(process, ip);
+ if (info == NULL)
+ return NULL;
+ else
+ return MC_file_object_info_find_function(info, ip);
+}
--- /dev/null
+/* Copyright (c) 2008-2014. The SimGrid Team.
+ * All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef MC_PROCESS_H
+#define MC_PROCESS_H
+
+#include "simgrid_config.h"
+
+#include <sys/types.h>
+
+#include "mc_forward.h"
+#include "mc_memory_map.h"
+
+SG_BEGIN_DECL()
+
+typedef enum {
+ MC_PROCESS_NO_FLAG = 0,
+ MC_PROCESS_SELF_FLAG = 1,
+} e_mc_process_flags_t;
+
+/** Representation of a process
+ */
+struct s_mc_process {
+ e_mc_process_flags_t process_flags;
+ pid_t pid;
+ memory_map_t memory_map;
+ void *maestro_stack_start, *maestro_stack_end;
+ char *libsimgrid_path;
+ mc_object_info_t libsimgrid_info;
+ mc_object_info_t binary_info;
+ mc_object_info_t object_infos[2];
+ size_t object_infos_size;
+};
+
+void MC_process_init(mc_process_t process, pid_t pid);
+void MC_process_clear(mc_process_t process);
+
+mc_object_info_t MC_process_find_object_info(mc_process_t process, void* ip);
+dw_frame_t MC_process_find_function(mc_process_t process, void* ip);
+
+SG_END_DECL()
+
+#endif
/* 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 <stdlib.h>
+
+#include <sys/types.h>
+
#include "mc_memory_map.h"
#include "mc_private.h"
-#include <stdlib.h>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory_map, mc,
"Logging specific to algorithms for memory_map");
-memory_map_t MC_get_memory_map(void)
+memory_map_t MC_get_memory_map(pid_t pid)
{
- FILE *fp; /* File pointer to process's proc maps file */
- char *line = NULL; /* Temporal storage for each line that is readed */
- ssize_t read; /* Number of bytes readed */
- size_t n = 0; /* Amount of bytes to read by xbt_getline */
- memory_map_t ret = NULL; /* The memory map to return */
-
-/* The following variables are used during the parsing of the file "maps" */
- s_map_region_t memreg; /* temporal map region used for creating the map */
- char *lfields[6], *tok, *endptr;
- int i;
-
-/* Open the actual process's proc maps file and create the memory_map_t */
-/* to be returned. */
- fp = fopen("/proc/self/maps", "r");
-
+ /* Open the actual process's proc maps file and create the memory_map_t */
+ /* to be returned. */
+ char* path = bprintf("/proc/%i/maps", (int) pid);
+ FILE *fp = fopen(path, "r");
+ free(path);
if(fp == NULL)
perror("fopen failed");
-
xbt_assert(fp,
- "Cannot open /proc/self/maps to investigate the memory map of the process. Please report this bug.");
-
+ "Cannot open /proc/self/maps to investigate the memory map of the process. Please report this bug.");
setbuf(fp, NULL);
- ret = xbt_new0(s_memory_map_t, 1);
+ memory_map_t ret = xbt_new0(s_memory_map_t, 1);
/* Read one line at the time, parse it and add it to the memory map to be returned */
+ ssize_t read; /* Number of bytes readed */
+ char* line = NULL;
+ size_t n = 0; /* Amount of bytes to read by xbt_getline */
while ((read = xbt_getline(&line, &n, fp)) != -1) {
//fprintf(stderr,"%s", line);
/* Tokenize the line using spaces as delimiters and store each token */
/* in lfields array. We expect 5 tokens/fields */
+ char* lfields[6];
lfields[0] = strtok(line, " ");
+ int i;
for (i = 1; i < 6 && lfields[i - 1] != NULL; i++) {
lfields[i] = strtok(NULL, " ");
}
/* Ok we are good enough to try to get the info we need */
/* First get the start and the end address of the map */
- tok = strtok(lfields[0], "-");
+ char *tok = strtok(lfields[0], "-");
if (tok == NULL)
xbt_abort();
+ s_map_region_t memreg; /* temporal map region used for creating the map */
+ char *endptr;
memreg.start_addr = (void *) strtoul(tok, &endptr, 16);
/* Make sure that the entire string was an hex number */
if (*endptr != '\0')
}
free(line);
-
fclose(fp);
-
return ret;
}
#include "../../src/include/mc/datatypes.h"
#include "../../src/mc/mc_object_info.h"
#include "../../src/mc/mc_private.h"
+#include "../../src/mc/mc_model_checker.h"
int test_some_array[4][5][6];
struct some_struct { int first; int second[4][5]; } test_some_struct;
}
static dw_variable_t test_global_variable(mc_object_info_t info, const char* name, void* address, long byte_size) {
+ mc_process_t process = &mc_model_checker->process;
+
dw_variable_t variable = find_global_variable_by_name(info, name);
xbt_assert(variable, "Global variable %s was not found", name);
xbt_assert(!strcmp(variable->name, name), "Name mismatch for %s", name);
xbt_assert(variable->address == address,
"Address mismatch for %s : %p expected but %p found", name, address, variable->address);
- dw_type_t type = xbt_dict_get_or_null(mc_binary_info->types, variable->type_origin);
+ dw_type_t type = xbt_dict_get_or_null(process->binary_info->types, variable->type_origin);
xbt_assert(type!=NULL, "Missing type for %s", name);
xbt_assert(type->byte_size = byte_size, "Byte size mismatch for %s", name);
return variable;
typedef struct foo {int i;} s_foo;
static void test_type_by_name(s_foo my_foo) {
- assert(xbt_dict_get_or_null(mc_binary_info->full_types_by_name, "struct foo"));
+ mc_process_t process = &mc_model_checker->process;
+ assert(xbt_dict_get_or_null(process->binary_info->full_types_by_name, "struct foo"));
}
int main(int argc, char** argv) {
dw_variable_t var;
dw_type_t type;
+
+ mc_process_t process = &mc_model_checker->process;
- test_global_variable(mc_binary_info, "some_local_variable", &some_local_variable, sizeof(int));
+ test_global_variable(process->binary_info, "some_local_variable", &some_local_variable, sizeof(int));
- var = test_global_variable(mc_binary_info, "test_some_array", &test_some_array, sizeof(test_some_array));
- type = xbt_dict_get_or_null(mc_binary_info->types, var->type_origin);
+ var = test_global_variable(process->binary_info, "test_some_array", &test_some_array, sizeof(test_some_array));
+ type = xbt_dict_get_or_null(process->binary_info->types, var->type_origin);
xbt_assert(type->element_count == 6*5*4, "element_count mismatch in test_some_array : %i / %i", type->element_count, 6*5*4);
- var = test_global_variable(mc_binary_info, "test_some_struct", &test_some_struct, sizeof(test_some_struct));
- type = xbt_dict_get_or_null(mc_binary_info->types, var->type_origin);
- assert(find_member(mc_binary_info, "first", type)->offset == 0);
- assert(find_member(mc_binary_info, "second", type)->offset
+ var = test_global_variable(process->binary_info, "test_some_struct", &test_some_struct, sizeof(test_some_struct));
+ type = xbt_dict_get_or_null(process->binary_info->types, var->type_origin);
+ assert(find_member(process->binary_info, "first", type)->offset == 0);
+ assert(find_member(process->binary_info, "second", type)->offset
== ((const char*)&test_some_struct.second) - (const char*)&test_some_struct);
unw_context_t context;
unw_getcontext(&context);
unw_init_local(&cursor, &context);
- test_local_variable(mc_binary_info, "main", "argc", &argc, &cursor);
+ test_local_variable(process->binary_info, "main", "argc", &argc, &cursor);
{
int lexical_block_variable = 50;
- test_local_variable(mc_binary_info, "main", "lexical_block_variable", &lexical_block_variable, &cursor);
+ test_local_variable(process->binary_info, "main", "lexical_block_variable", &lexical_block_variable, &cursor);
}
s_foo my_foo;
#! ./tesh
$ $SG_TEST_EXENV ${bindir:=.}/dwarf
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> WARNING: This test depends on the MPI's eager limit. Set it appropriately.
> Initializing (0 of 3)
> (0) is alive on Tremblay
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/coll_selector' to 'mpich'
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_global/INFO] Get debug information ...
-> [0.000000] [mc_global/INFO] Get debug information done !
+> [0.000000] [mc_process/INFO] Get debug information ...
+> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
