/********************************* Global *************************************/
XBT_ATTRIB_NORETURN XBT_PUBLIC void MC_run();
-XBT_PUBLIC void MC_process_clock_add(smx_actor_t, double);
-XBT_PUBLIC double MC_process_clock_get(smx_actor_t);
XBT_PRIVATE void MC_automaton_load(const char *file);
/********************************* Memory *************************************/
SG_END_DECL
+#ifdef __cplusplus
+XBT_PUBLIC void MC_process_clock_add(const simgrid::kernel::actor::ActorImpl*, double);
+XBT_PUBLIC double MC_process_clock_get(const simgrid::kernel::actor::ActorImpl*);
+#endif
+
#endif
session->log_state();
}
-bool ModelChecker::handle_message(char* buffer, ssize_t size)
+bool ModelChecker::handle_message(const char* buffer, ssize_t size)
{
s_mc_message_t base_message;
xbt_assert(size >= (ssize_t)sizeof(base_message), "Broken message");
private:
void setup_ignore();
- bool handle_message(char* buffer, ssize_t size);
+ bool handle_message(const char* buffer, ssize_t size);
void handle_waitpid();
void on_signal(int signo);
{
while (states_.size() > (std::size_t)_sg_mc_max_visited_states) {
XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
- auto min_element = boost::range::min_element(states_,
- [](std::unique_ptr<simgrid::mc::VisitedState>& a, std::unique_ptr<simgrid::mc::VisitedState>& b) {
- return a->num < b->num;
- });
+ auto min_element = boost::range::min_element(
+ states_, [](const std::unique_ptr<simgrid::mc::VisitedState>& a,
+ const std::unique_ptr<simgrid::mc::VisitedState>& b) { return a->num < b->num; });
xbt_assert(min_element != states_.end());
// and drop it:
states_.erase(min_element);
/********** Static functions ***********/
-static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1,
- simgrid::mc::PatternCommunication* comm2)
+static e_mc_comm_pattern_difference_t compare_comm_pattern(const simgrid::mc::PatternCommunication* comm1,
+ const simgrid::mc::PatternCommunication* comm2)
{
if(comm1->type != comm2->type)
return TYPE_DIFF;
}
static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process,
- simgrid::mc::PatternCommunication* comm, unsigned int cursor)
+ const simgrid::mc::PatternCommunication* comm, unsigned int cursor)
{
char* type;
char* res;
namespace simgrid {
namespace mc {
-void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, PatternCommunication* comm,
+void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, const PatternCommunication* comm,
int backtracking)
{
if (not backtracking) {
std::vector<PatternCommunication*>& incomplete_pattern = incomplete_communications_pattern[issuer];
auto current_comm_pattern =
std::find_if(begin(incomplete_pattern), end(incomplete_pattern),
- [&comm_addr](PatternCommunication* comm) { return remote(comm->comm_addr) == comm_addr; });
+ [&comm_addr](const PatternCommunication* comm) { return remote(comm->comm_addr) == comm_addr; });
if (current_comm_pattern == std::end(incomplete_pattern))
xbt_die("Corresponding communication not found!");
void prepare();
void real_run();
void log_state() override;
- void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking);
+ void deterministic_comm_pattern(int process, const simgrid::mc::PatternCommunication* comm, int backtracking);
void restoreState();
public:
// These are used by functions which should be moved in CommunicationDeterminismChecker:
this->atomic_propositions = std::move(atomic_propositions);
}
-static bool evaluate_label(xbt_automaton_exp_label_t l, std::vector<int> const& values)
+static bool evaluate_label(const xbt_automaton_exp_label* l, std::vector<int> const& values)
{
switch (l->type) {
case xbt_automaton_exp_label::AUT_OR:
return trace;
}
-std::shared_ptr<Pair> LivenessChecker::create_pair(Pair* current_pair, xbt_automaton_state_t state,
+std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt_automaton_state_t state,
std::shared_ptr<const std::vector<int>> propositions)
{
expanded_pairs_count_++;
void remove_acceptance_pair(int pair_num);
void purge_visited_pairs();
void backtrack();
- std::shared_ptr<Pair> create_pair(Pair* pair, xbt_automaton_state_t state,
+ std::shared_ptr<Pair> create_pair(const Pair* pair, xbt_automaton_state_t state,
std::shared_ptr<const std::vector<int>> propositions);
// A stack of (application_state, automaton_state) pairs for DFS exploration:
namespace simgrid {
namespace mc {
-void SafetyChecker::check_non_termination(State* current_state)
+void SafetyChecker::check_non_termination(const State* current_state)
{
for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
if (snapshot_equal((*state)->system_state_.get(), current_state->system_state_.get())) {
void log_state() override;
private:
- void check_non_termination(simgrid::mc::State* current_state);
+ void check_non_termination(const State* current_state);
void backtrack();
void restore_state();
std::vector<Type*> types;
std::size_t heapsize = 0;
- void initHeapInformation(xbt_mheap_t heap, const std::vector<IgnoredHeapRegion>& i);
+ void initHeapInformation(const s_xbt_mheap_t* heap, const std::vector<IgnoredHeapRegion>& i);
};
class StateComparator {
compared_pointers.clear();
}
- int initHeapInformation(xbt_mheap_t heap1, xbt_mheap_t heap2, const std::vector<IgnoredHeapRegion>& i1,
- const std::vector<IgnoredHeapRegion>& i2);
+ int initHeapInformation(const s_xbt_mheap_t* heap1, const s_xbt_mheap_t* heap2,
+ const std::vector<IgnoredHeapRegion>& i1, const std::vector<IgnoredHeapRegion>& i2);
template <int rank> HeapArea& equals_to_(std::size_t i, std::size_t j)
{
this->equals_to_<2>(b2, f2).block_ == b1 && this->equals_to_<2>(b2, f2).fragment_ == f1;
}
- void match_equals(HeapLocationPairs* list);
+ void match_equals(const HeapLocationPairs* list);
};
} // namespace mc
namespace simgrid {
namespace mc {
-void StateComparator::match_equals(HeapLocationPairs* list)
+void StateComparator::match_equals(const HeapLocationPairs* list)
{
for (auto const& pair : *list) {
if (pair[0].fragment_ != -1) {
}
}
-void ProcessComparisonState::initHeapInformation(xbt_mheap_t heap, const std::vector<IgnoredHeapRegion>& i)
+void ProcessComparisonState::initHeapInformation(const s_xbt_mheap_t* heap, const std::vector<IgnoredHeapRegion>& i)
{
auto heaplimit = heap->heaplimit;
this->heapsize = heap->heapsize;
this->types.assign(heaplimit * MAX_FRAGMENT_PER_BLOCK, nullptr);
}
-int StateComparator::initHeapInformation(xbt_mheap_t heap1, xbt_mheap_t heap2, const std::vector<IgnoredHeapRegion>& i1,
+int StateComparator::initHeapInformation(const s_xbt_mheap_t* heap1, const s_xbt_mheap_t* heap2,
+ const std::vector<IgnoredHeapRegion>& i1,
const std::vector<IgnoredHeapRegion>& i2)
{
if ((heap1->heaplimit != heap2->heaplimit) || (heap1->heapsize != heap2->heapsize))
malloc_info heapinfo_temp2;
malloc_info heapinfo_temp2b;
- Region* heap_region1 = MC_get_heap_region(snapshot1);
- Region* heap_region2 = MC_get_heap_region(snapshot2);
+ const Region* heap_region1 = MC_get_heap_region(snapshot1);
+ const Region* heap_region2 = MC_get_heap_region(snapshot2);
// This is the address of std_heap->heapinfo in the application process:
void* heapinfo_address = &((xbt_mheap_t)process.heap_address)->heapinfo;
HeapLocationPairs* previous, int size, int check_ignore)
{
const RemoteClient& process = mc_model_checker->process();
- Region* heap_region1 = MC_get_heap_region(snapshot1);
- Region* heap_region2 = MC_get_heap_region(snapshot2);
+ const Region* heap_region1 = MC_get_heap_region(snapshot1);
+ const Region* heap_region2 = MC_get_heap_region(snapshot2);
for (int i = 0; i < size; ) {
if (check_ignore > 0) {
*/
static bool heap_area_differ_with_type(StateComparator& state, const void* real_area1, const void* real_area2,
const Snapshot& snapshot1, const Snapshot& snapshot2,
- HeapLocationPairs* previous, Type* type, int area_size, int check_ignore,
+ HeapLocationPairs* previous, const Type* type, int area_size, int check_ignore,
int pointer_level)
{
// HACK: This should not happen but in practice, there are some
const void* addr_pointed1;
const void* addr_pointed2;
- Region* heap_region1 = MC_get_heap_region(snapshot1);
- Region* heap_region2 = MC_get_heap_region(snapshot2);
+ const Region* heap_region1 = MC_get_heap_region(snapshot1);
+ const Region* heap_region2 = MC_get_heap_region(snapshot2);
switch (type->type) {
case DW_TAG_unspecified_type:
return true;
}
} else {
- for (simgrid::mc::Member& member : type->members) {
+ for (const simgrid::mc::Member& member : type->members) {
// TODO, optimize this? (for the offset case)
const void* real_member1 = dwarf::resolve_member(real_area1, type, &member, &snapshot1);
const void* real_member2 = dwarf::resolve_member(real_area2, type, &member, &snapshot2);
return nullptr;
}
- for (simgrid::mc::Member& member : type->members) {
+ for (const simgrid::mc::Member& member : type->members) {
if (member.has_offset_location()) {
// We have the offset, use it directly (shortcut):
if (member.offset() == offset)
type_size = type->byte_size;
}
- simgrid::mc::Region* heap_region1 = MC_get_heap_region(snapshot1);
- simgrid::mc::Region* heap_region2 = MC_get_heap_region(snapshot2);
+ const Region* heap_region1 = MC_get_heap_region(snapshot1);
+ const Region* heap_region2 = MC_get_heap_region(snapshot2);
const malloc_info* heapinfo1 =
(const malloc_info*)heap_region1->read(&heapinfo_temp1, &heapinfos1[block1], sizeof(malloc_info));
static bool areas_differ_with_type(simgrid::mc::StateComparator& state, const void* real_area1,
const simgrid::mc::Snapshot& snapshot1, simgrid::mc::Region* region1,
const void* real_area2, const simgrid::mc::Snapshot& snapshot2,
- simgrid::mc::Region* region2, simgrid::mc::Type* type, int pointer_level)
+ simgrid::mc::Region* region2, const simgrid::mc::Type* type, int pointer_level)
{
const simgrid::mc::Type* subtype;
const simgrid::mc::Type* subsubtype;
}
case DW_TAG_structure_type:
case DW_TAG_class_type:
- for (simgrid::mc::Member& member : type->members) {
+ for (const simgrid::mc::Member& member : type->members) {
const void* member1 = simgrid::dwarf::resolve_member(real_area1, type, &member, &snapshot1);
const void* member2 = simgrid::dwarf::resolve_member(real_area2, type, &member, &snapshot2);
simgrid::mc::Region* subregion1 = snapshot1.get_region(member1, region1); // region1 is hinted
return false;
}
-static bool global_variables_differ(simgrid::mc::StateComparator& state, simgrid::mc::ObjectInformation* object_info,
- simgrid::mc::Region* r1, simgrid::mc::Region* r2,
- const simgrid::mc::Snapshot& snapshot1, const simgrid::mc::Snapshot& snapshot2)
+static bool global_variables_differ(simgrid::mc::StateComparator& state,
+ const simgrid::mc::ObjectInformation* object_info, simgrid::mc::Region* r1,
+ simgrid::mc::Region* r2, const simgrid::mc::Snapshot& snapshot1,
+ const simgrid::mc::Snapshot& snapshot2)
{
xbt_assert(r1 && r2, "Missing region.");
/** Resolve a location expression */
Location resolve(simgrid::dwarf::DwarfExpression const& expression, simgrid::mc::ObjectInformation* object_info,
- unw_cursor_t* c, void* frame_pointer_address, simgrid::mc::AddressSpace* address_space)
+ unw_cursor_t* c, void* frame_pointer_address, const simgrid::mc::AddressSpace* address_space)
{
simgrid::dwarf::ExpressionContext context;
context.frame_base = frame_pointer_address;
}
Location resolve(simgrid::dwarf::LocationList const& locations, simgrid::mc::ObjectInformation* object_info,
- unw_cursor_t* c, void* frame_pointer_address, simgrid::mc::AddressSpace* address_space)
+ unw_cursor_t* c, void* frame_pointer_address, const simgrid::mc::AddressSpace* address_space)
{
unw_word_t ip = 0;
if (c && unw_get_reg(c, UNW_REG_IP, &ip))
return simgrid::dwarf::resolve(*expression, object_info, c, frame_pointer_address, address_space);
}
-LocationList location_list(simgrid::mc::ObjectInformation& info, Dwarf_Attribute& attr)
+LocationList location_list(const simgrid::mc::ObjectInformation& info, Dwarf_Attribute& attr)
{
LocationList locations;
std::ptrdiff_t offset = 0;
XBT_PRIVATE
Location resolve(simgrid::dwarf::DwarfExpression const& expression, simgrid::mc::ObjectInformation* object_info,
- unw_cursor_t* c, void* frame_pointer_address, simgrid::mc::AddressSpace* address_space);
+ unw_cursor_t* c, void* frame_pointer_address, const simgrid::mc::AddressSpace* address_space);
Location resolve(simgrid::dwarf::LocationList const& locations, simgrid::mc::ObjectInformation* object_info,
- unw_cursor_t* c, void* frame_pointer_address, simgrid::mc::AddressSpace* address_space);
+ unw_cursor_t* c, void* frame_pointer_address, const simgrid::mc::AddressSpace* address_space);
XBT_PRIVATE
-simgrid::dwarf::LocationList location_list(simgrid::mc::ObjectInformation& info, Dwarf_Attribute& attr);
+simgrid::dwarf::LocationList location_list(const simgrid::mc::ObjectInformation& info, Dwarf_Attribute& attr);
} // namespace dwarf
} // namespace simgrid
const char* name);
/** Augment the current module with informations about the other ones */
-XBT_PRIVATE void postProcessObjectInformation(simgrid::mc::RemoteClient* process, simgrid::mc::ObjectInformation* info);
+XBT_PRIVATE void postProcessObjectInformation(const simgrid::mc::RemoteClient* process,
+ simgrid::mc::ObjectInformation* info);
} // namespace mc
} // namespace simgrid
* @param unit the DIE of the compile unit of the current DIE
* @param frame containing frame if any
*/
-static void MC_dwarf_handle_variable_die(simgrid::mc::ObjectInformation* info, Dwarf_Die* die, Dwarf_Die* unit,
+static void MC_dwarf_handle_variable_die(simgrid::mc::ObjectInformation* info, Dwarf_Die* die, const Dwarf_Die* unit,
simgrid::mc::Frame* frame, const char* ns);
/** @brief Get the DW_TAG_type of the DIE
* @param member the member of the type
* @param child DIE of the member (DW_TAG_member)
*/
-static void MC_dwarf_fill_member_location(simgrid::mc::Type* type, simgrid::mc::Member* member, Dwarf_Die* child)
+static void MC_dwarf_fill_member_location(const simgrid::mc::Type* type, simgrid::mc::Member* member, Dwarf_Die* child)
{
xbt_assert(not dwarf_hasattr(child, DW_AT_data_bit_offset), "Can't groke DW_AT_data_bit_offset.");
* @param unit DIE of the compilation unit containing the type DIE
* @param type the type
*/
-static void MC_dwarf_add_members(simgrid::mc::ObjectInformation* /*info*/, Dwarf_Die* die, Dwarf_Die* /*unit*/,
- simgrid::mc::Type* type)
+static void MC_dwarf_add_members(const simgrid::mc::ObjectInformation* /*info*/, Dwarf_Die* die,
+ const Dwarf_Die* /*unit*/, simgrid::mc::Type* type)
{
int res;
Dwarf_Die child;
static int mc_anonymous_variable_index = 0;
static std::unique_ptr<simgrid::mc::Variable> MC_die_to_variable(simgrid::mc::ObjectInformation* info, Dwarf_Die* die,
- Dwarf_Die* /*unit*/, simgrid::mc::Frame* frame,
- const char* ns)
+ const Dwarf_Die* /*unit*/,
+ const simgrid::mc::Frame* frame, const char* ns)
{
// Skip declarations:
if (MC_dwarf_attr_flag(die, DW_AT_declaration, false))
return variable;
}
-static void MC_dwarf_handle_variable_die(simgrid::mc::ObjectInformation* info, Dwarf_Die* die, Dwarf_Die* unit,
+static void MC_dwarf_handle_variable_die(simgrid::mc::ObjectInformation* info, Dwarf_Die* die, const Dwarf_Die* unit,
simgrid::mc::Frame* frame, const char* ns)
{
std::unique_ptr<simgrid::mc::Variable> variable = MC_die_to_variable(info, die, unit, frame, ns);
/*************************************************************************/
-void postProcessObjectInformation(RemoteClient* process, ObjectInformation* info)
+void postProcessObjectInformation(const RemoteClient* process, ObjectInformation* info)
{
for (auto& t : info->types) {
Type* type = &(t.second);
XBT_PRIVATE const char* attrname(int attr);
XBT_PRIVATE const char* tagname(int tag);
-XBT_PRIVATE void* resolve_member(const void* base, simgrid::mc::Type* type, simgrid::mc::Member* member,
+XBT_PRIVATE void* resolve_member(const void* base, const simgrid::mc::Type* type, const simgrid::mc::Member* member,
const simgrid::mc::AddressSpace* snapshot);
XBT_PRIVATE
* @param snapshot Snapshot (or nullptr)
* @return Process address of the given member of the 'object' struct/class
*/
-void* resolve_member(const void* base, simgrid::mc::Type* /*type*/, simgrid::mc::Member* member,
+void* resolve_member(const void* base, const simgrid::mc::Type* /*type*/, const simgrid::mc::Member* member,
const simgrid::mc::AddressSpace* address_space)
{
ExpressionContext state;
while (not simix_global->actors_to_run.empty()) {
simix_global->run_all_actors();
for (smx_actor_t const& process : simix_global->actors_that_ran) {
- smx_simcall_t req = &process->simcall;
+ const s_smx_simcall* req = &process->simcall;
if (req->call_ != SIMCALL_NONE && not simgrid::mc::request_is_visible(req))
process->simcall_handle(0);
}
/* This is the list of requests that are visible from the checker algorithm.
* Any other requests are handled right away on the application side.
*/
-bool request_is_visible(smx_simcall_t req)
+bool request_is_visible(const s_smx_simcall* req)
{
#if SIMGRID_HAVE_MC
xbt_assert(mc_model_checker == nullptr, "This should be called from the client side");
XBT_PRIVATE bool actor_is_enabled(smx_actor_t process);
/** Check if the given simcall is visible */
-XBT_PRIVATE bool request_is_visible(smx_simcall_t req);
-
+XBT_PRIVATE bool request_is_visible(const s_smx_simcall* req);
}
}
DATA_DIFF,
};
-static inline e_mc_call_type_t MC_get_call_type(smx_simcall_t req)
+static inline e_mc_call_type_t MC_get_call_type(const s_smx_simcall* req)
{
switch (req->call_) {
case SIMCALL_COMM_ISEND:
}
#endif
-double MC_process_clock_get(smx_actor_t process)
+double MC_process_clock_get(const simgrid::kernel::actor::ActorImpl* process)
{
if (simgrid::mc::processes_time.empty())
return 0;
return -1;
}
-void MC_process_clock_add(smx_actor_t process, double amount)
+void MC_process_clock_add(const simgrid::kernel::actor::ActorImpl* process, double amount)
{
simgrid::mc::processes_time[process->get_pid()] += amount;
}
smx_actor_t process = SIMIX_process_from_PID(transition.pid_);
if (not process)
xbt_die("Unexpected process (pid:%d).", transition.pid_);
- smx_simcall_t simcall = &(process->simcall);
+ const s_smx_simcall* simcall = &(process->simcall);
if (simcall == nullptr || simcall->call_ == SIMCALL_NONE)
xbt_die("No simcall for process %d.", transition.pid_);
if (not simgrid::mc::request_is_visible(simcall) || not simgrid::mc::actor_is_enabled(process))
* @param target Local vector (to be filled with copies of `s_smx_actor_t`)
* @param remote_dynar Address of the process dynar in the remote list
*/
-static void MC_process_refresh_simix_actor_dynar(simgrid::mc::RemoteClient* process,
+static void MC_process_refresh_simix_actor_dynar(const simgrid::mc::RemoteClient* process,
std::vector<simgrid::mc::ActorInformation>& target,
simgrid::mc::RemotePtr<s_xbt_dynar_t> remote_dynar)
{
explicit State(unsigned long state_number);
std::size_t interleave_size() const;
- void add_interleaving_set(smx_actor_t actor) { this->actor_states_[actor->get_pid()].consider(); }
+ void add_interleaving_set(const simgrid::kernel::actor::ActorImpl* actor)
+ {
+ this->actor_states_[actor->get_pid()].consider();
+ }
Transition get_transition() const;
};
}
return instance_.get();
}
-void Client::handle_deadlock_check(s_mc_message_t*)
+void Client::handle_deadlock_check(const s_mc_message_t*)
{
bool deadlock = false;
if (not simix_global->process_list.empty()) {
s_mc_message_int_t answer{MC_MESSAGE_DEADLOCK_CHECK_REPLY, deadlock};
xbt_assert(channel_.send(answer) == 0, "Could not send response");
}
-void Client::handle_continue(s_mc_message_t*)
+void Client::handle_continue(const s_mc_message_t*)
{
/* Nothing to do */
}
-void Client::handle_simcall(s_mc_message_simcall_handle_t* message)
+void Client::handle_simcall(const s_mc_message_simcall_handle_t* message)
{
smx_actor_t process = SIMIX_process_from_PID(message->pid);
if (not process)
xbt_die("Could not send MESSAGE_WAITING to model-checker");
}
-void Client::handle_actor_enabled(s_mc_message_actor_enabled_t* msg)
+void Client::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg)
{
bool res = simgrid::mc::actor_is_enabled(SIMIX_process_from_PID(msg->aid));
s_mc_message_int_t answer{MC_MESSAGE_ACTOR_ENABLED_REPLY, res};
if (received_size < 0)
xbt_die("Could not receive commands from the model-checker");
- s_mc_message_t* message = (s_mc_message_t*)message_buffer;
+ const s_mc_message_t* message = (s_mc_message_t*)message_buffer;
switch (message->type) {
case MC_MESSAGE_DEADLOCK_CHECK:
xbt_assert(received_size == sizeof(s_mc_message_t), "Unexpected size for DEADLOCK_CHECK (%zd != %zu)",
void handle_messages();
private:
- void handle_deadlock_check(s_mc_message_t* msg);
- void handle_continue(s_mc_message_t* msg);
- void handle_simcall(s_mc_message_simcall_handle_t* message);
- void handle_actor_enabled(s_mc_message_actor_enabled_t* msg);
+ void handle_deadlock_check(const s_mc_message_t* msg);
+ void handle_continue(const s_mc_message_t* msg);
+ void handle_simcall(const s_mc_message_simcall_handle_t* message);
+ void handle_actor_enabled(const s_mc_message_actor_enabled_t* msg);
public:
Channel const& get_channel() const { return channel_; }
* @param page_count Number of pages of the region
* @return Snapshot page numbers of this new snapshot
*/
-ChunkedData::ChunkedData(PageStore& store, AddressSpace& as, RemotePtr<void> addr, std::size_t page_count)
+ChunkedData::ChunkedData(PageStore& store, const AddressSpace& as, RemotePtr<void> addr, std::size_t page_count)
: store_(&store)
{
this->pagenos_.resize(page_count);
/** Get a a pointer to a chunk */
void* page(std::size_t i) const { return store_->get_page(pagenos_[i]); }
- ChunkedData(PageStore& store, AddressSpace& as, RemotePtr<void> addr, std::size_t page_count);
+ ChunkedData(PageStore& store, const AddressSpace& as, RemotePtr<void> addr, std::size_t page_count);
};
} // namespace mc
}
/** Store a page in memory */
-std::size_t PageStore::store_page(void* page)
+std::size_t PageStore::store_page(const void* page)
{
xbt_assert(top_index_ <= this->capacity_, "top_index is not consistent");
void ref_page(size_t pageno);
/** @brief Store a page in the page store */
- std::size_t store_page(void* page);
+ std::size_t store_page(const void* page);
/** @brief Get a page from its page number
*
}
}
-static XBT_ALWAYS_INLINE void* mc_translate_address_region(uintptr_t addr, simgrid::mc::Region* region)
+static XBT_ALWAYS_INLINE void* mc_translate_address_region(uintptr_t addr, const simgrid::mc::Region* region)
{
auto split = simgrid::mc::mmu::split(addr - region->start().address());
auto pageno = split.first;
return (char*)snapshot_page + offset;
}
-void* Region::read(void* target, const void* addr, std::size_t size)
+void* Region::read(void* target, const void* addr, std::size_t size) const
{
xbt_assert(contain(simgrid::mc::remote(addr)), "Trying to read out of the region boundary.");
* @param region2 Region of the address in the second snapshot
* @return same semantic as memcmp
*/
-int MC_snapshot_region_memcmp(const void* addr1, simgrid::mc::Region* region1, const void* addr2,
- simgrid::mc::Region* region2, size_t size)
+int MC_snapshot_region_memcmp(const void* addr1, const simgrid::mc::Region* region1, const void* addr2,
+ const simgrid::mc::Region* region2, size_t size)
{
// Using alloca() for large allocations may trigger stack overflow:
// use malloc if the buffer is too big.
* @param size Size of the data to read in bytes
* @return Pointer where the data is located (either target buffer or original location)
*/
- void* read(void* target, const void* addr, std::size_t size);
+ void* read(void* target, const void* addr, std::size_t size) const;
};
} // namespace mc
} // namespace simgrid
-int MC_snapshot_region_memcmp(const void* addr1, simgrid::mc::Region* region1, const void* addr2,
- simgrid::mc::Region* region2, std::size_t size);
+int MC_snapshot_region_memcmp(const void* addr1, const simgrid::mc::Region* region1, const void* addr2,
+ const simgrid::mc::Region* region2, std::size_t size);
-static XBT_ALWAYS_INLINE void* MC_region_read_pointer(simgrid::mc::Region* region, const void* addr)
+static XBT_ALWAYS_INLINE void* MC_region_read_pointer(const simgrid::mc::Region* region, const void* addr)
{
void* res;
return *(void**)region->read(&res, addr, sizeof(void*));
* @param ip Instruction pointer
* @return true if the variable is valid
* */
-static bool valid_variable(simgrid::mc::Variable* var, simgrid::mc::Frame* scope, const void* ip)
+static bool valid_variable(const simgrid::mc::Variable* var, simgrid::mc::Frame* scope, const void* ip)
{
// The variable is not yet valid:
if (scope->range.begin() + var->start_scope > (std::uint64_t)ip)
if (not scope || not scope->range.contain(stack_frame->ip))
return;
- for (Variable& current_variable : scope->variables) {
+ for (const Variable& current_variable : scope->variables) {
if (not valid_variable(¤t_variable, scope, (void*)stack_frame->ip))
continue;
snapshot->process()->clear_bytes(remote(region.addr), region.size);
}
-static void snapshot_ignore_restore(simgrid::mc::Snapshot* snapshot)
+static void snapshot_ignore_restore(const simgrid::mc::Snapshot* snapshot)
{
for (auto const& ignored_data : snapshot->ignored_data_)
snapshot->process()->write_bytes(ignored_data.data.data(), ignored_data.data.size(), remote(ignored_data.start));
void* Snapshot::read_bytes(void* buffer, std::size_t size, RemotePtr<void> address, ReadOptions options) const
{
- Region* region = this->get_region((void*)address.address());
+ const Region* region = this->get_region((void*)address.address());
if (region) {
void* res = region->read(buffer, (void*)address.address(), size);
if (buffer == res || options & ReadOptions::lazy())