#define SIMGRID_MC_VISITED_STATE_HPP
#include "src/mc/mc_state.hpp"
-#include "src/mc/sosp/mc_snapshot.hpp"
+#include "src/mc/sosp/Snapshot.hpp"
#include <cstddef>
#include <memory>
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_smx.hpp"
-#include "src/mc/sosp/mc_snapshot.hpp"
+#include "src/mc/sosp/Snapshot.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt, "Logging specific to mc_compare in mc");
#include "src/mc/mc_safety.hpp"
#include "src/mc/mc_smx.hpp"
#include "src/mc/remote/Client.hpp"
-#include "src/mc/sosp/mc_snapshot.hpp"
+#include "src/mc/sosp/Snapshot.hpp"
#include "xbt/backtrace.hpp"
#include <libunwind.h>
* under the terms of the license (GNU LGPL) which comes with this package. */
#include <cinttypes>
-
#include <cstdint>
#include "xbt/log.h"
#include "mc/datatypes.h"
#include "src/mc/mc_hash.hpp"
#include "src/mc/mc_private.hpp"
-#include "src/mc/sosp/mc_snapshot.hpp"
+#include "src/mc/sosp/Snapshot.hpp"
#include <mc/mc.h>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_hash, mc, "Logging specific to mc_hash");
#ifndef SIMGRID_MC_STATE_HPP
#define SIMGRID_MC_STATE_HPP
-#include "src/mc/sosp/mc_snapshot.hpp"
#include "src/kernel/activity/CommImpl.hpp"
#include "src/mc/Transition.hpp"
+#include "src/mc/sosp/Snapshot.hpp"
namespace simgrid {
namespace mc {
#include "src/mc/remote/RemoteClient.hpp"
+#include "src/mc/mc_smx.hpp"
+#include "src/mc/sosp/Snapshot.hpp"
#include "xbt/file.hpp"
#include "xbt/log.h"
-#include "src/mc/mc_smx.hpp"
-#include "src/mc/sosp/mc_snapshot.hpp"
#include <fcntl.h>
#include <libunwind-ptrace.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. */
-#include <cstdlib>
-
-#include <sys/mman.h>
-#ifdef __FreeBSD__
-#define MAP_POPULATE MAP_PREFAULT_READ
-#endif
-
#include "src/mc/ModelChecker.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_forward.hpp"
#include "src/mc/mc_smx.hpp"
-#include "src/mc/sosp/RegionSnapshot.hpp"
+#include "src/mc/sosp/Region.hpp"
+
+#include <cstdlib>
+#include <sys/mman.h>
+#ifdef __FreeBSD__
+#define MAP_POPULATE MAP_PREFAULT_READ
+#endif
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_RegionSnaphot, mc, "Logging specific to region snapshots");
void* target_page = (void*)simgrid::mc::mmu::join(i, (std::uintptr_t)(void*)start().address());
const void* source_page = get_chunks().page(i);
mc_model_checker->process().write_bytes(source_page, xbt_pagesize, remote(target_page));
- }
+ }
}
} // namespace mc
}
RegionSnapshot& operator=(RegionSnapshot&& that)
{
- region_type_ = that.region_type_;
- object_info_ = that.object_info_;
- start_addr_ = that.start_addr_;
- size_ = that.size_;
- chunks_ = std::move(that.chunks_);
+ region_type_ = that.region_type_;
+ object_info_ = that.object_info_;
+ start_addr_ = that.start_addr_;
+ size_ = that.size_;
+ chunks_ = std::move(that.chunks_);
that.clear();
return *this;
}
void clear()
{
- region_type_ = UnknownRegion;
+ region_type_ = UnknownRegion;
chunks_.clear();
- object_info_ = nullptr;
- start_addr_ = nullptr;
- size_ = 0;
+ object_info_ = nullptr;
+ start_addr_ = nullptr;
+ size_ = 0;
}
ChunkedData const& get_chunks() const { return chunks_; }
/* 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 <cstddef> /* std::size_t */
-
+#include "src/mc/sosp/Snapshot.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_hash.hpp"
#include "src/mc/mc_smx.hpp"
-#include "src/mc/sosp/mc_snapshot.hpp"
+
+#include <cstddef> /* std::size_t */
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_snapshot, mc, "Taking and restoring snapshots");
{
// Using alloca() for large allocations may trigger stack overflow:
// use malloc if the buffer is too big.
- bool stack_alloc = size < 64;
+ bool stack_alloc = size < 64;
void* buffer1a = stack_alloc ? alloca(size) : ::operator new(size);
void* buffer2a = stack_alloc ? alloca(size) : ::operator new(size);
const void* buffer1 = MC_region_read(region1, buffer1a, addr1, size);
void* end_heap = heap->breakval;
add_region(simgrid::mc::RegionType::Heap, nullptr, start_heap, (char*)end_heap - (char*)start_heap);
- heap_bytes_used_ = mmalloc_get_bytes_used_remote(heap->heaplimit, process->get_malloc_info());
+ heap_bytes_used_ = mmalloc_get_bytes_used_remote(heap->heaplimit, process->get_malloc_info());
}
/** @brief Checks whether the variable is in scope for a given IP.
}
Snapshot::Snapshot(int num_state, RemoteClient* process)
- : AddressSpace(process)
- , num_state_(num_state)
- , heap_bytes_used_(0)
- , enabled_processes_()
- , hash_(0)
+ : AddressSpace(process), num_state_(num_state), heap_bytes_used_(0), enabled_processes_(), hash_(0)
{
XBT_DEBUG("Taking snapshot %i", num_state);
#include "src/mc/ModelChecker.hpp"
#include "src/mc/inspect/mc_unw.hpp"
#include "src/mc/remote/RemoteClient.hpp"
-#include "src/mc/sosp/RegionSnapshot.hpp"
+#include "src/mc/sosp/Region.hpp"
// ***** Snapshot region
xbt_assert(region->contain(simgrid::mc::remote(addr)), "Trying to read out of the region boundary.");
- // Last byte of the region:
- void* end = (char*)addr + size - 1;
- if (simgrid::mc::mmu::same_chunk((std::uintptr_t)addr, (std::uintptr_t)end)) {
- // The memory is contained in a single page:
- return mc_translate_address_region((uintptr_t)addr, region);
- }
- // Otherwise, the memory spans several pages:
- return MC_region_read_fragmented(region, target, addr, size);
+ // Last byte of the region:
+ void* end = (char*)addr + size - 1;
+ if (simgrid::mc::mmu::same_chunk((std::uintptr_t)addr, (std::uintptr_t)end)) {
+ // The memory is contained in a single page:
+ return mc_translate_address_region((uintptr_t)addr, region);
+ }
+ // Otherwise, the memory spans several pages:
+ return MC_region_read_fragmented(region, target, addr, size);
}
static XBT_ALWAYS_INLINE void* MC_region_read_pointer(simgrid::mc::RegionSnapshot* region, const void* addr)
#include "src/include/catch.hpp"
#include "src/mc/mc_config.hpp"
-#include "src/mc/sosp/mc_snapshot.hpp"
+#include "src/mc/sosp/Snapshot.hpp"
#include <cstddef>
#include <random>
src/mc/sosp/PageStore.cpp
src/mc/sosp/ChunkedData.hpp
src/mc/sosp/ChunkedData.cpp
- src/mc/sosp/RegionSnapshot.cpp
- src/mc/sosp/RegionSnapshot.hpp
- src/mc/sosp/mc_snapshot.hpp
- src/mc/sosp/mc_snapshot.cpp
+ src/mc/sosp/Region.cpp
+ src/mc/sosp/Region.hpp
+ src/mc/sosp/Snapshot.hpp
+ src/mc/sosp/Snapshot.cpp
src/mc/AddressSpace.hpp
src/mc/ModelChecker.hpp
src/xbt/dynar_test.cpp
src/xbt/xbt_str_test.cpp)
if (SIMGRID_HAVE_MC)
- set(UNIT_TESTS ${UNIT_TESTS} src/mc/sosp/mc_snapshot_test.cpp src/mc/sosp/PageStore_test.cpp)
+ set(UNIT_TESTS ${UNIT_TESTS} src/mc/sosp/Snapshot_test.cpp src/mc/sosp/PageStore_test.cpp)
else()
- set(EXTRA_DIST ${EXTRA_DIST} src/mc/sosp/mc_snapshot_test.cpp src/mc/sosp/PageStore_test.cpp)
+ set(EXTRA_DIST ${EXTRA_DIST} src/mc/sosp/Snapshot_test.cpp src/mc/sosp/PageStore_test.cpp)
endif()
add_executable (unit-tests ${UNIT_TESTS})