, page_store_(500)
, process_(std::move(process))
{
-
}
-ModelChecker::~ModelChecker() {
+ModelChecker::~ModelChecker()
+{
if (socket_event_ != nullptr)
event_free(socket_event_);
if (signal_event_ != nullptr)
{
XBT_DEBUG("Shuting down model-checker");
- simgrid::mc::RemoteClient* process = &this->process();
+ RemoteClient* process = &this->process();
if (process->running()) {
XBT_DEBUG("Killing process");
kill(process->pid(), SIGKILL);
}
}
-void ModelChecker::resume(simgrid::mc::RemoteClient& process)
+void ModelChecker::resume(RemoteClient& process)
{
int res = process.get_channel().send(MC_MESSAGE_CONTINUE);
if (res)
- throw simgrid::xbt::errno_error();
+ throw xbt::errno_error();
process.clear_cache();
}
XBT_INFO("Counter-example execution trace:");
for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
XBT_INFO(" %s", s.c_str());
- simgrid::mc::dumpRecordPath();
- simgrid::mc::session->log_state();
+ dumpRecordPath();
+ session->log_state();
if (xbt_log_no_loc) {
XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
} else {
XBT_INFO("Counter-example execution trace:");
for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
XBT_INFO(" %s", s.c_str());
- simgrid::mc::dumpRecordPath();
- simgrid::mc::session->log_state();
+ dumpRecordPath();
+ session->log_state();
}
bool ModelChecker::handle_message(char* buffer, ssize_t size)
memcpy(&base_message, buffer, sizeof(base_message));
switch(base_message.type) {
-
case MC_MESSAGE_IGNORE_HEAP:
{
s_mc_message_ignore_heap_t message;
xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
XBT_DEBUG("Received symbol: %s", message.name);
- if (simgrid::mc::property_automaton == nullptr)
- simgrid::mc::property_automaton = xbt_automaton_new();
+ if (property_automaton == nullptr)
+ property_automaton = xbt_automaton_new();
- simgrid::mc::RemoteClient* process = &this->process();
- simgrid::mc::RemotePtr<int> address = simgrid::mc::remote((int*)message.data);
- simgrid::xbt::add_proposition(simgrid::mc::property_automaton, message.name,
- [process, address]() { return process->read(address); });
+ RemoteClient* process = &this->process();
+ RemotePtr<int> address = remote((int*)message.data);
+ xbt::add_proposition(property_automaton, message.name, [process, address]() { return process->read(address); });
break;
}
default:
xbt_die("Unexpected message from model-checked application");
-
}
return true;
}
}
if (pid == this->process().pid()) {
-
// From PTRACE_O_TRACEEXIT:
#ifdef __linux__
if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
return message.value != 0;
}
-}
-}
+} // namespace mc
+} // namespace simgrid
mc_model_checker->setChecker(this);
}
-}
-}
+} // namespace mc
+} // namespace simgrid
/* If this is a new state (or if we don't care about state-equality reduction) */
if (visited_state_ == nullptr) {
-
/* Get an enabled process and insert it in the interleave set of the next state */
for (auto& remoteActor : mc_model_checker->process().actors()) {
auto actor = remoteActor.copy.get_buffer();
intptr_t second;
switch (atom) {
-
// Registers:
-
case DW_OP_breg0:
case DW_OP_breg1:
case DW_OP_breg2:
namespace simgrid {
namespace mc {
-/* For an executable object, addresses are virtual address
- * (there is no offset) i.e.
- * \f$\text{virtual address} = \{dwarf address}\f$
+/* For an executable object, addresses are virtual address (there is no offset) i.e.
+ * \f$\text{virtual address} = \{dwarf address}\f$
*
- * For a shared object, the addresses are offset from the beginning
- * of the shared object (the base address of the mapped shared
- * object must be used as offset
+ * For a shared object, the addresses are offset from the beginning 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$.
*/
if (this->executable())
return nullptr;
- // For an a shared-object (ET_DYN, including position-independent executables)
- // the base address is its lowest address:
+ // For an a shared-object (ET_DYN, including position-independent executables) the base address is its lowest address:
void* result = this->start_exec;
if (this->start_rw != nullptr && result > (void*)this->start_rw)
result = this->start_rw;
return result;
}
-simgrid::mc::Frame* ObjectInformation::find_function(const void* ip) const
+Frame* ObjectInformation::find_function(const void* ip) const
{
/* This is implemented by binary search on a sorted array.
*
* We could use std::binary_search by including the high_pc inside
* the FunctionIndexEntry.
*/
- const simgrid::mc::FunctionIndexEntry* base = this->functions_index.data();
- int i = 0;
- int j = this->functions_index.size() - 1;
+ const FunctionIndexEntry* base = this->functions_index.data();
+ int i = 0;
+ int j = this->functions_index.size() - 1;
while (j >= i) {
int k = i + ((j - i) / 2);
return nullptr;
}
-const simgrid::mc::Variable* ObjectInformation::find_variable(const char* name) const
+const Variable* ObjectInformation::find_variable(const char* name) const
{
- for (simgrid::mc::Variable const& variable : this->global_variables) {
+ for (Variable const& variable : this->global_variables) {
if (variable.name == name)
return &variable;
}
while (first <= last) {
size_type cursor = first + (last - first) / 2;
- simgrid::mc::Variable& current_var = this->global_variables[cursor];
+ Variable& current_var = this->global_variables[cursor];
int cmp = current_var.name.compare(name);
if (cmp == 0) {
-
// Find the whole range:
first = cursor;
while (first != 0 && this->global_variables[first - 1].name == name)
/** Ignore a local variable in a scope
*
- * Ignore all instances of variables with a given name in
- * any (possibly inlined) subprogram with a given namespaced
+ * Ignore all instances of variables with a given name in any (possibly inlined) subprogram with a given namespaced
* name.
*
* @param var_name Name of the local variable to ignore
* @param subprogram (possibly inlined) Subprogram of the scope current scope
* @param scope Current scope
*/
-static void remove_local_variable(simgrid::mc::Frame& scope, const char* var_name, const char* subprogram_name,
- simgrid::mc::Frame const& subprogram)
+static void remove_local_variable(Frame& scope, const char* var_name, const char* subprogram_name,
+ Frame const& subprogram)
{
typedef std::vector<Variable>::size_type size_type;
// If the current subprogram matches the given name:
if ((subprogram_name == nullptr || (not subprogram.name.empty() && subprogram.name == subprogram_name)) &&
not scope.variables.empty()) {
-
// Try to find the variable and remove it:
size_type start = 0;
size_type end = scope.variables.size() - 1;
// Binary search:
while (start <= end) {
size_type cursor = start + (end - start) / 2;
- simgrid::mc::Variable& current_var = scope.variables[cursor];
+ Variable& current_var = scope.variables[cursor];
int compare = current_var.name.compare(var_name);
if (compare == 0) {
// Variable found, remove it:
}
// And recursive processing in nested scopes:
- for (simgrid::mc::Frame& nested_scope : scope.scopes) {
+ for (Frame& nested_scope : scope.scopes) {
// The new scope may be an inlined subroutine, in this case we want to use its
// namespaced name in recursive calls:
- simgrid::mc::Frame const& nested_subprogram =
- nested_scope.tag == DW_TAG_inlined_subroutine ? nested_scope : subprogram;
+ Frame const& nested_subprogram = nested_scope.tag == DW_TAG_inlined_subroutine ? nested_scope : subprogram;
remove_local_variable(nested_scope, var_name, subprogram_name, nested_subprogram);
}
}
void ObjectInformation::remove_local_variable(const char* var_name, const char* subprogram_name)
{
for (auto& entry : this->subprograms)
- simgrid::mc::remove_local_variable(entry.second, var_name, subprogram_name, entry.second);
+ mc::remove_local_variable(entry.second, var_name, subprogram_name, entry.second);
}
/** @brief Fills the position of the segments (executable, read-only, read/write) */
// TODO, use the ELF segment information for more robustness
-void find_object_address(std::vector<simgrid::xbt::VmMap> const& maps, simgrid::mc::ObjectInformation* result)
+void find_object_address(std::vector<xbt::VmMap> const& maps, ObjectInformation* result)
{
const int PROT_RW = PROT_READ | PROT_WRITE;
const int PROT_RX = PROT_READ | PROT_EXEC;
- std::string name = simgrid::xbt::Path(result->file_name).get_base_name();
+ std::string name = xbt::Path(result->file_name).get_base_name();
for (size_t i = 0; i < maps.size(); ++i) {
simgrid::xbt::VmMap const& reg = maps[i];
else if (reg.prot == PROT_READ) {
xbt_assert(not result->start_ro,
"Multiple read-only segments for %s, not supported. Compiling with the following may help: "
- "-Wl,-znorelro -Wl,-znoseparate-code",
+ "-Wl,-znorelro -Wl,-znoseparate-code",
maps[i].pathname.c_str());
result->start_ro = (char*)reg.start_addr;
result->end_ro = (char*)reg.end_addr;
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)",
received_size, sizeof(s_mc_message_t));
if (channel_.send(message))
xbt_die("Could not send STACK_REGION to model-checker");
}
-}
-}
+} // namespace mc
+} // namespace simgrid
/** @brief Compute a hash for the given memory page
*
- * The page is used before inserting the page in the page store
- * in order to find duplicate of this page in the page store.
+ * The page is used before inserting the page in the page store in order to find duplicate of this page in the page
+ * store.
*
* @param data Memory page
* @return hash off the page
std::size_t PageStore::alloc_page()
{
if (this->free_pages_.empty()) {
-
// Expand the region:
if (this->top_index_ == this->capacity_)
// All the pages are allocated, we need add more pages:
// Use a page from the top:
return this->top_index_++;
-
} else {
-
// Use a page from free_pages_ (inside of the region):
size_t res = this->free_pages_[this->free_pages_.size() - 1];
this->free_pages_.pop_back();
for (size_t const& pageno : page_set) {
const void* snapshot_page = this->get_page(pageno);
if (memcmp(page, snapshot_page, xbt_pagesize) == 0) {
-
// If a page with the same content is already in the page store it's reused and its refcount is incremented.
page_counts_[pageno]++;
return pageno;
/************************************* Take Snapshot ************************************/
/****************************************************************************************/
-void simgrid::mc::Snapshot::snapshot_regions(simgrid::mc::RemoteClient* process)
+void Snapshot::snapshot_regions(RemoteClient* process)
{
snapshot_regions_.clear();
for (auto const& object_info : process->object_infos)
- add_region(simgrid::mc::RegionType::Data, object_info.get(), object_info->start_rw,
- object_info->end_rw - object_info->start_rw);
+ add_region(RegionType::Data, object_info.get(), object_info->start_rw, object_info->end_rw - object_info->start_rw);
xbt_mheap_t heap = process->get_heap();
void* start_heap = heap->base;
void* end_heap = heap->breakval;
- add_region(simgrid::mc::RegionType::Heap, nullptr, start_heap, (char*)end_heap - (char*)start_heap);
+ add_region(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());
}
return true;
}
-static void fill_local_variables_values(mc_stack_frame_t stack_frame, simgrid::mc::Frame* scope,
+static void fill_local_variables_values(mc_stack_frame_t stack_frame, Frame* scope,
std::vector<s_local_variable_t>& result)
{
if (not scope || not scope->range.contain(stack_frame->ip))
return;
- for (simgrid::mc::Variable& current_variable : scope->variables) {
-
+ for (Variable& current_variable : scope->variables) {
if (not valid_variable(¤t_variable, scope, (void*)stack_frame->ip))
continue;
if (current_variable.address != nullptr)
new_var.address = current_variable.address;
else if (not current_variable.location_list.empty()) {
- simgrid::dwarf::Location location = simgrid::dwarf::resolve(
- current_variable.location_list, current_variable.object_info, &(stack_frame->unw_cursor),
- (void*)stack_frame->frame_base, &mc_model_checker->process());
+ dwarf::Location location = simgrid::dwarf::resolve(current_variable.location_list, current_variable.object_info,
+ &(stack_frame->unw_cursor), (void*)stack_frame->frame_base,
+ &mc_model_checker->process());
if (not location.in_memory())
xbt_die("Cannot handle non-address variable");
new_var.address = location.address();
-
} else
xbt_die("No address");
}
// Recursive processing of nested scopes:
- for (simgrid::mc::Frame& nested_scope : scope->scopes)
+ for (Frame& nested_scope : scope->scopes)
fill_local_variables_values(stack_frame, &nested_scope, result);
}
return variables;
}
-static std::vector<s_mc_stack_frame_t> unwind_stack_frames(simgrid::mc::UnwindContext* stack_context)
+static std::vector<s_mc_stack_frame_t> unwind_stack_frames(UnwindContext* stack_context)
{
- simgrid::mc::RemoteClient* process = &mc_model_checker->process();
+ RemoteClient* process = &mc_model_checker->process();
std::vector<s_mc_stack_frame_t> result;
unw_cursor_t c = stack_context->cursor();
// TODO, check condition check (unw_init_local==0 means end of frame)
while (1) {
-
s_mc_stack_frame_t stack_frame;
stack_frame.unw_cursor = c;
// TODO, use real addresses in frame_t instead of fixing it here
- simgrid::mc::Frame* frame = process->find_function(remote(ip));
+ Frame* frame = process->find_function(remote(ip));
stack_frame.frame = frame;
if (frame) {
return result;
}
-void simgrid::mc::Snapshot::snapshot_stacks(simgrid::mc::RemoteClient* process)
+void Snapshot::snapshot_stacks(RemoteClient* process)
{
for (auto const& stack : process->stack_areas()) {
s_mc_snapshot_stack_t st;
}
}
-static void snapshot_handle_ignore(simgrid::mc::Snapshot* snapshot)
+static void snapshot_handle_ignore(Snapshot* snapshot)
{
xbt_assert(snapshot->process());
for (auto const& region : snapshot->process()->ignored_regions())
snapshot->process()->clear_bytes(remote(region.addr), region.size);
}
+
static void snapshot_ignore_restore(simgrid::mc::Snapshot* snapshot)
{
for (auto const& ignored_data : snapshot->ignored_data_)
void Snapshot::add_region(RegionType type, ObjectInformation* object_info, void* start_addr, std::size_t size)
{
- if (type == simgrid::mc::RegionType::Data)
+ if (type == RegionType::Data)
xbt_assert(object_info, "Missing object info for object.");
- else if (type == simgrid::mc::RegionType::Heap)
+ else if (type == RegionType::Heap)
xbt_assert(not object_info, "Unexpected object info for heap region.");
- simgrid::mc::Region* region = new Region(type, start_addr, size);
+ Region* region = new Region(type, start_addr, size);
region->object_info(object_info);
- snapshot_regions_.push_back(std::unique_ptr<simgrid::mc::Region>(std::move(region)));
+ snapshot_regions_.push_back(std::unique_ptr<Region>(std::move(region)));
}
void* Snapshot::read_bytes(void* buffer, std::size_t size, RemotePtr<void> address, ReadOptions options) const
XBT_DEBUG("Restore snapshot %i", num_state_);
// Restore regions
- for (std::unique_ptr<simgrid::mc::Region> const& region : snapshot_regions_) {
+ for (std::unique_ptr<Region> const& region : snapshot_regions_) {
if (region) // privatized variables are not snapshotted
region.get()->restore();
}
