[mc] Fix mc_translate_address_region() for per-page snapshots

It was completely broken :/

diff --git a/src/mc/mc_page_store.cpp b/src/mc/mc_page_store.cpp
index e095e85..467ade6 100644 (file)
--- a/src/mc/mc_page_store.cpp
+++ b/src/mc/mc_page_store.cpp
@@ -162,6 +162,11 @@ size_t s_mc_pages_store::store_page(void* page)
 
 extern "C" {
 
 
 extern "C" {
 

+const void* mc_page_store_get_page(mc_pages_store_t page_store, size_t pageno)
+{
+  return page_store->get_page(pageno);
+}
+

 mc_pages_store_t mc_pages_store_new()
 {
   return new s_mc_pages_store_t(500);
 mc_pages_store_t mc_pages_store_new()
 {
   return new s_mc_pages_store_t(500);

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 1752d63..2aefccf 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -149,6 +149,7 @@ void mc_softdirty_reset();
 
 typedef struct s_mc_pages_store s_mc_pages_store_t, * mc_pages_store_t;
 mc_pages_store_t mc_pages_store_new();
 
 typedef struct s_mc_pages_store s_mc_pages_store_t, * mc_pages_store_t;
 mc_pages_store_t mc_pages_store_new();

+const void* mc_page_store_get_page(mc_pages_store_t page_store, size_t pageno);

 
 static inline bool mc_snapshot_region_linear(mc_mem_region_t region) {
   return !region || !region->data;
 
 static inline bool mc_snapshot_region_linear(mc_mem_region_t region) {
   return !region || !region->data;

diff --git a/src/mc/mc_snapshot.c b/src/mc/mc_snapshot.c
index 79cfd78..38820c9 100644 (file)
--- a/src/mc/mc_snapshot.c
+++ b/src/mc/mc_snapshot.c
@@ -36,8 +36,10 @@ void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region)
 
   // Per-page snapshot:
   else if (region->page_numbers) {
 
   // Per-page snapshot:
   else if (region->page_numbers) {

-    size_t pageno = mc_page_number(region->data, (void*) addr);
-    return (char*) region->page_numbers[pageno] + mc_page_offset((void*) addr);
+    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);

   }
 
   else {
   }
 
   else {


@@ -55,7 +57,6 @@ void* mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot)
 
   mc_mem_region_t region = mc_get_snapshot_region((void*) addr, snapshot);
   return mc_translate_address_region(addr, region);
 
   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
 }
 
 /** @brief Read memory from a snapshot region broken across fragmented pages