From 15ab58c0b9a3d96ed52f5db885b72724a96af934 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 26 Jun 2014 14:10:38 +0200 Subject: [PATCH 1/1] [mc] Inline mc_translate_address() and mc_translate_address_region() --- src/mc/mc_private.h | 17 ---------------- src/mc/mc_snapshot.c | 48 +++++++++++++++++++++++++++++--------------- 2 files changed, 32 insertions(+), 33 deletions(-) diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index d46b8ed003..ef2afff19e 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -180,23 +180,6 @@ typedef struct s_mc_model_checker { extern mc_model_checker_t mc_model_checker; -void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region); - -/** \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 - * */ -void* mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot); - extern xbt_dynar_t mc_checkpoint_ignore; /********************************* MC Global **********************************/ diff --git a/src/mc/mc_snapshot.c b/src/mc/mc_snapshot.c index 07c10079e2..7f3629145b 100644 --- a/src/mc/mc_snapshot.c +++ b/src/mc/mc_snapshot.c @@ -25,8 +25,39 @@ mc_mem_region_t mc_get_snapshot_region(void* addr, mc_snapshot_t snapshot) return NULL; } +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) { @@ -41,10 +72,7 @@ void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region) // Per-page snapshot: else if (region->page_numbers) { - 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); + return mc_translate_address_region(addr, region); } else { @@ -52,18 +80,6 @@ void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region) } } -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); - return mc_translate_address_region(addr, region); -} - /** @brief Read memory from a snapshot region broken across fragmented pages * * @param addr Process (non-snapshot) address of the data -- 2.20.1