+ s_mc_location_list_t frame_base;
+ xbt_dynar_t /* <dw_variable_t> */ variables; /* Cannot use dict, there may be several variables with the same name (in different lexical blocks)*/
+ unsigned long int id; /* DWARF offset of the subprogram */
+ xbt_dynar_t /* <dw_frame_t> */ scopes;
+ Dwarf_Off abstract_origin_id;
+ mc_object_info_t object_info;
+};
+
+struct s_mc_function_index_item {
+ void* low_pc, *high_pc;
+ dw_frame_t function;
+};
+
+void mc_frame_free(dw_frame_t freme);
+
+void dw_type_free(dw_type_t t);
+void dw_variable_free(dw_variable_t v);
+void dw_variable_free_voidp(void *t);
+
+void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t variable);
+void MC_register_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable);
+void MC_dwarf_register_non_global_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable);
+void MC_dwarf_register_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable);
+
+/** Find the DWARF offset for this ELF object
+ *
+ * An offset is applied to address found in DWARF:
+ *
+ * <ul>
+ * <li>for an executable obejct, addresses are virtual address
+ * (there is no offset) i.e. \f$\text{virtual address} = \{dwarf address}\f$;</li>
+ * <li>for a shared object, the addreses are offset from the begining
+ * of the shared object (the base address of the mapped shared
+ * object must be used as offset
+ * i.e. \f$\text{virtual address} = \text{shared object base address}
+ * + \text{dwarf address}\f$.</li>
+ *
+ */
+void* MC_object_base_address(mc_object_info_t info);
+
+/********************************** DWARF **********************************/
+
+#define MC_EXPRESSION_STACK_SIZE 64
+
+#define MC_EXPRESSION_OK 0
+#define MC_EXPRESSION_E_UNSUPPORTED_OPERATION 1
+#define MC_EXPRESSION_E_STACK_OVERFLOW 2
+#define MC_EXPRESSION_E_STACK_UNDERFLOW 3
+#define MC_EXPRESSION_E_MISSING_STACK_CONTEXT 4
+#define MC_EXPRESSION_E_MISSING_FRAME_BASE 5
+#define MC_EXPRESSION_E_NO_BASE_ADDRESS 6
+
+typedef struct s_mc_expression_state {
+ uintptr_t stack[MC_EXPRESSION_STACK_SIZE];
+ size_t stack_size;
+
+ unw_cursor_t* cursor;
+ void* frame_base;
+ mc_snapshot_t snapshot;
+ mc_object_info_t object_info;
+} s_mc_expression_state_t, *mc_expression_state_t;
+
+int mc_dwarf_execute_expression(size_t n, const Dwarf_Op* ops, mc_expression_state_t state);
+
+void* mc_find_frame_base(dw_frame_t frame, mc_object_info_t object_info, unw_cursor_t* unw_cursor);
+
+/********************************** Miscellaneous **********************************/
+
+typedef struct s_local_variable{
+ dw_frame_t subprogram;
+ unsigned long ip;
+ char *name;
+ dw_type_t type;
+ void *address;
+ int region;
+}s_local_variable_t, *local_variable_t;
+
+/********************************* Communications pattern ***************************/
+
+typedef struct s_mc_comm_pattern{
+ int num;
+ smx_action_t comm;
+ e_smx_comm_type_t type;
+ unsigned long src_proc;
+ unsigned long dst_proc;
+ const char *src_host;
+ const char *dst_host;
+ char *rdv;
+ ssize_t data_size;
+ void *data;
+}s_mc_comm_pattern_t, *mc_comm_pattern_t;
+
+extern xbt_dynar_t initial_communications_pattern;
+extern xbt_dynar_t communications_pattern;
+extern xbt_dynar_t incomplete_communications_pattern;
+
+void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, int call);
+void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm);
+void MC_pre_modelcheck_comm_determinism(void);
+void MC_modelcheck_comm_determinism(void);
+
+/* *********** Sets *********** */
+
+typedef struct s_mc_address_set *mc_address_set_t;
+
+mc_address_set_t mc_address_set_new();
+void mc_address_set_free(mc_address_set_t* p);
+void mc_address_add(mc_address_set_t p, const void* value);
+bool mc_address_test(mc_address_set_t p, const void* value);
+
+/* *********** Hash *********** */
+
+/** \brief Hash the current state
+ * \param num_state number of states
+ * \param stacks stacks (mc_snapshot_stak_t) used fot the stack unwinding informations
+ * \result resulting hash
+ * */
+uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks);
+
+/* *********** Snapshot *********** */
+
+static inline __attribute__((always_inline))
+void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region)
+{
+ size_t pageno = mc_page_number(region->start_addr, (void*) addr);
+ size_t snapshot_pageno = region->page_numbers[pageno];
+ const void* snapshot_page = mc_page_store_get_page(mc_model_checker->pages, snapshot_pageno);
+ return (char*) snapshot_page + mc_page_offset((void*) addr);
+}
+
+/** \brief Translate a pointer from process address space to snapshot address space
+ *
+ * The address space contains snapshot of the main/application memory:
+ * this function finds the address in a given snaphot for a given
+ * real/application address.
+ *
+ * For read only memory regions and other regions which are not int the
+ * snapshot, the address is not changed.
+ *
+ * \param addr Application address
+ * \param snapshot The snapshot of interest (if NULL no translation is done)
+ * \return Translated address in the snapshot address space
+ * */
+static inline __attribute__((always_inline))
+void* mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot)
+{
+
+ // If not in a process state/clone:
+ if (!snapshot) {
+ return (uintptr_t *) addr;
+ }
+
+ mc_mem_region_t region = mc_get_snapshot_region((void*) addr, snapshot);
+
+ xbt_assert(mc_region_contain(region, (void*) addr), "Trying to read out of the region boundary.");
+
+ if (!region) {
+ return (void *) addr;
+ }
+
+ // Flat snapshot:
+ else if (region->data) {
+ uintptr_t offset = addr - (uintptr_t) region->start_addr;
+ return (void *) ((uintptr_t) region->data + offset);
+ }
+
+ // Per-page snapshot:
+ else if (region->page_numbers) {
+ return mc_translate_address_region(addr, region);
+ }
+
+ else {
+ xbt_die("No data for this memory region");
+ }
+}
+
+static inline __attribute__ ((always_inline))
+ void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) {
+ if(snapshot==NULL)
+ xbt_die("snapshot is NULL");
+ void** addr = &((xbt_mheap_t)std_heap)->breakval;
+ return mc_snapshot_read_pointer(addr, snapshot);
+}
+
+static inline __attribute__ ((always_inline))
+void* mc_snapshot_read_pointer(void* addr, mc_snapshot_t snapshot)
+{
+ void* res;
+ return *(void**) mc_snapshot_read(addr, snapshot, &res, sizeof(void*));
+}
+
+/** @brief Read memory from a snapshot region
+ *
+ * @param addr Process (non-snapshot) address of the data
+ * @param region Snapshot memory region where the data is located
+ * @param target Buffer to store the value
+ * @param size Size of the data to read in bytes
+ * @return Pointer where the data is located (target buffer of original location)
+ */
+static inline __attribute__((always_inline))
+void* mc_snapshot_read_region(void* addr, mc_mem_region_t region, void* target, size_t size)
+{
+ uintptr_t offset = (uintptr_t) addr - (uintptr_t) region->start_addr;
+
+ xbt_assert(addr >= region->start_addr && (char*) addr+size < (char*)region->start_addr+region->size,
+ "Trying to read out of the region boundary.");
+
+ // Linear memory region:
+ if (region->data) {
+ return (void*) ((uintptr_t) region->data + offset);
+ }
+
+ // Fragmented memory region:
+ else if (region->page_numbers) {
+ void* end = (char*) addr + size - 1;
+ if( mc_same_page(addr, end) ) {
+ // The memory is contained in a single page:
+ return mc_translate_address_region((uintptr_t) addr, region);
+ } else {
+ // The memory spans several pages:
+ return mc_snapshot_read_fragmented(addr, region, target, size);
+ }
+ }
+
+ else {
+ xbt_die("No data available for this region");
+ }
+}
+
+
+SG_END_DECL()