Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' of github.com:mquinson/simgrid
authorMartin Quinson <martin.quinson@loria.fr>
Mon, 7 Mar 2016 09:03:05 +0000 (10:03 +0100)
committerMartin Quinson <martin.quinson@loria.fr>
Mon, 7 Mar 2016 09:03:05 +0000 (10:03 +0100)
24 files changed:
src/mc/ModelChecker.cpp
src/mc/PageStore.cpp
src/mc/Process.cpp
src/mc/RegionSnapshot.cpp
src/mc/mc_base.cpp
src/mc/mc_checkpoint.cpp
src/mc/mc_comm_determinism.cpp
src/mc/mc_comm_pattern.cpp
src/mc/mc_compare.cpp
src/mc/mc_config.cpp
src/mc/mc_diff.cpp
src/mc/mc_dwarf.cpp
src/mc/mc_global.cpp
src/mc/mc_ignore.cpp
src/mc/mc_liveness.cpp
src/mc/mc_memory.cpp
src/mc/mc_mmu.h
src/mc/mc_protocol.cpp
src/mc/mc_request.cpp
src/mc/mc_safety.cpp
src/mc/mc_smx.cpp
src/mc/mc_snapshot.cpp
src/mc/mc_state.cpp
src/mc/mc_visited.cpp

index 15f6d23..0d97a64 100644 (file)
@@ -319,9 +319,8 @@ bool ModelChecker::handle_events()
         throw simgrid::xbt::errno_error(errno);
       return handle_message(buffer, size);
     }
-    if (socket_pollfd->revents & POLLERR) {
+    if (socket_pollfd->revents & POLLERR)
       throw_socket_error(socket_pollfd->fd);
-    }
     if (socket_pollfd->revents & POLLHUP)
       xbt_die("Socket hang up?");
   }
@@ -331,9 +330,8 @@ bool ModelChecker::handle_events()
       this->handle_signals();
       return true;
     }
-    if (signalfd_pollfd->revents & POLLERR) {
+    if (signalfd_pollfd->revents & POLLERR)
       throw_socket_error(signalfd_pollfd->fd);
-    }
     if (signalfd_pollfd->revents & POLLHUP)
       xbt_die("Signalfd hang up?");
   }
@@ -427,10 +425,9 @@ void ModelChecker::on_signal(const struct signalfd_siginfo* info)
 void ModelChecker::wait_client(simgrid::mc::Process& process)
 {
   this->resume(process);
-  while (this->process().running()) {
+  while (this->process().running())
     if (!this->handle_events())
       return;
-  }
 }
 
 void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value)
@@ -442,10 +439,9 @@ void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long p
   m.value = value;
   process.send_message(m);
   process.cache_flags = (mc_process_cache_flags_t) 0;
-  while (process.running()) {
+  while (process.running())
     if (!this->handle_events())
       return;
-  }
 }
 
 }
index 7f7e166..3289157 100644 (file)
@@ -39,9 +39,8 @@ PageStore::hash_type mc_hash_page(const void* data)
 
   // This djb2:
   std::uint64_t hash = 5381;
-  for (std::size_t i = 0; i != n; ++i) {
+  for (std::size_t i = 0; i != n; ++i)
     hash = ((hash << 5) + hash) + values[i];
-  }
   return hash;
 }
 
@@ -54,9 +53,8 @@ PageStore::PageStore(size_t size) :
   // by relocating it somewhere else in the virtual memory
   // space:
   void* memory = ::mmap(nullptr, size << xbt_pagebits, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS|MAP_POPULATE, -1, 0);
-  if (memory == MAP_FAILED) {
+  if (memory == MAP_FAILED)
     xbt_die("Could not mmap initial snapshot pages.");
-  }
 
   this->top_index_ = 0;
   this->capacity_ = size;
@@ -77,9 +75,8 @@ void PageStore::resize(std::size_t size)
   // Expand the memory region by moving it into another
   // virtual memory address if necessary:
   void* new_memory = mremap(this->memory_, old_bytesize, new_bytesize, MREMAP_MAYMOVE);
-  if (new_memory == MAP_FAILED) {
+  if (new_memory == MAP_FAILED)
     xbt_die("Could not mremap snapshot pages.");
-  }
 
   this->capacity_ = size;
   this->memory_ = new_memory;
@@ -95,10 +92,9 @@ std::size_t PageStore::alloc_page()
   if (this->free_pages_.empty()) {
 
     // Expand the region:
-    if (this->top_index_ == this->capacity_) {
+    if (this->top_index_ == this->capacity_)
       // All the pages are allocated, we need add more pages:
       this->resize(2 * this->capacity_);
-    }
 
     // Use a page from the top:
     return this->top_index_++;
index 5360933..80fa3f2 100644 (file)
@@ -130,9 +130,9 @@ static ssize_t pread_whole(int fd, void *buf, size_t count, std::uint64_t offset
       count  -= res;
       buffer += res;
       offset += res;
-    } else if (res==0) {
+    } else if (res==0)
       return -1;
-    else if (errno != EINTR) {
+    else if (errno != EINTR) {
       perror("pread_whole");
       return -1;
     }
@@ -150,11 +150,10 @@ static ssize_t pwrite_whole(int fd, const void *buf, size_t count, off_t offset)
       count  -= res;
       buffer += res;
       offset += res;
-    } else if (res==0) {
+    } else if (res==0)
       return -1;
-    } else if (errno != EINTR) {
+    else if (errno != EINTR)
       return -1;
-    }
   }
   return real_count;
 }
@@ -247,9 +246,8 @@ Process::~Process()
   this->maestro_stack_start_ = nullptr;
   this->maestro_stack_end_ = nullptr;
 
-  if (this->memory_file >= 0) {
+  if (this->memory_file >= 0)
     close(this->memory_file);
-  }
 
   if (this->unw_underlying_addr_space != unw_local_addr_space) {
     unw_destroy_addr_space(this->unw_underlying_addr_space);
@@ -389,34 +387,28 @@ void Process::init_memory_map_info()
 
 std::shared_ptr<simgrid::mc::ObjectInformation> Process::find_object_info(RemotePtr<void> addr) const
 {
-  for (auto const& object_info : this->object_infos) {
+  for (auto const& object_info : this->object_infos)
     if (addr.address() >= (std::uint64_t)object_info->start
-        && addr.address() <= (std::uint64_t)object_info->end) {
+        && addr.address() <= (std::uint64_t)object_info->end)
       return object_info;
-    }
-  }
   return nullptr;
 }
 
 std::shared_ptr<ObjectInformation> Process::find_object_info_exec(RemotePtr<void> addr) const
 {
-  for (std::shared_ptr<ObjectInformation> const& info : this->object_infos) {
+  for (std::shared_ptr<ObjectInformation> const& info : this->object_infos)
     if (addr.address() >= (std::uint64_t) info->start_exec
-        && addr.address() <= (std::uint64_t) info->end_exec) {
+        && addr.address() <= (std::uint64_t) info->end_exec)
       return info;
-    }
-  }
   return nullptr;
 }
 
 std::shared_ptr<ObjectInformation> Process::find_object_info_rw(RemotePtr<void> addr) const
 {
-  for (std::shared_ptr<ObjectInformation> const& info : this->object_infos) {
+  for (std::shared_ptr<ObjectInformation> const& info : this->object_infos)
     if (addr.address() >= (std::uint64_t)info->start_rw
-        && addr.address() <= (std::uint64_t)info->end_rw) {
+        && addr.address() <= (std::uint64_t)info->end_rw)
       return info;
-    }
-  }
   return nullptr;
 }
 
@@ -589,16 +581,14 @@ void Process::ignore_region(std::uint64_t addr, std::size_t size)
 
   std::size_t position;
   if (current_region->addr == addr) {
-    if (current_region->size < size) {
+    if (current_region->size < size)
       position = cursor + 1;
-    } else {
+    else
       position = cursor;
-    }
-  } else if (current_region->addr < addr) {
+  } else if (current_region->addr < addr)
     position = cursor + 1;
-  } else {
+  else
     position = cursor;
-  }
   ignored_regions_.insert(
     ignored_regions_.begin() + position, region);
 }
index bfcc7ba..333aed2 100644 (file)
@@ -119,11 +119,10 @@ RegionSnapshot region(
   RegionType type, void *start_addr, void* permanent_addr, size_t size,
   RegionSnapshot const* ref_region)
 {
-  if (_sg_mc_sparse_checkpoint) {
+  if (_sg_mc_sparse_checkpoint)
     return sparse_region(type, start_addr, permanent_addr, size, ref_region);
-  } else  {
+  else
     return dense_region(type, start_addr, permanent_addr, size);
-  }
 }
 
 RegionSnapshot sparse_region(RegionType region_type,
index e8f1bb4..9717dfc 100644 (file)
@@ -91,12 +91,11 @@ int MC_request_is_enabled(smx_simcall_t req)
        * communication is not ready, it can timeout and won't block. */
       if (_sg_mc_timeout == 1)
         return TRUE;
-    } else {
-      /* On the other hand if it hasn't a timeout, check if the comm is ready.*/
-      if (act->comm.detached && act->comm.src_proc == nullptr
+    }
+    /* On the other hand if it hasn't a timeout, check if the comm is ready.*/
+    else if (act->comm.detached && act->comm.src_proc == nullptr
           && act->comm.type == SIMIX_COMM_READY)
         return (act->comm.dst_proc != nullptr);
-    }
     return (act->comm.src_proc && act->comm.dst_proc);
 
   case SIMCALL_COMM_WAITANY: {
@@ -112,9 +111,9 @@ int MC_request_is_enabled(smx_simcall_t req)
       assert(comms_buffer.elmsize == sizeof(act));
       buffer_size = comms_buffer.elmsize * comms_buffer.used;
       comms = &comms_buffer;
-    } else {
+    } else
       comms = simcall_comm_waitany__get__comms(req);
-    }
+
     // Read all the dynar buffer:
     char buffer[buffer_size];
     if (mc_mode == MC_MODE_SERVER)
@@ -210,10 +209,8 @@ static int prng_random(int min, int max)
 
 int simcall_HANDLER_mc_random(smx_simcall_t simcall, int min, int max)
 {
-  if (!MC_is_active() && !MC_record_path){
+  if (!MC_is_active() && !MC_record_path)
     return prng_random(min, max);
-  }
-
   return simcall->mc_value;
 }
 
index 38b4e44..c831100 100644 (file)
@@ -155,13 +155,11 @@ static void get_memory_regions(simgrid::mc::Process* process, mc_snapshot_t snap
   const size_t n = process->object_infos.size();
   snapshot->snapshot_regions.resize(n + 1);
   int i = 0;
-  for (auto const& object_info : process->object_infos) {
-    add_region(i, snapshot, simgrid::mc::RegionType::Data,
+  for (auto const& object_info : process->object_infos)
+    add_region(i++, snapshot, simgrid::mc::RegionType::Data,
       object_info.get(),
       object_info->start_rw, object_info->start_rw,
       object_info->end_rw - object_info->start_rw);
-    ++i;
-  }
 
   xbt_mheap_t heap = process->get_heap();
   void *start_heap = heap->base;
@@ -175,16 +173,14 @@ static void get_memory_regions(simgrid::mc::Process* process, mc_snapshot_t snap
     process->get_malloc_info());
 
 #ifdef HAVE_SMPI
-  if (mc_model_checker->process().privatized() && MC_smpi_process_count()) {
+  if (mc_model_checker->process().privatized() && MC_smpi_process_count())
     // snapshot->privatization_index = smpi_loaded_page
     mc_model_checker->process().read_variable(
       "smpi_loaded_page", &snapshot->privatization_index,
       sizeof(snapshot->privatization_index));
-  else
+  else
 #endif
-  {
     snapshot->privatization_index = simgrid::mc::ProcessIndexMissing;
-  }
 }
 
 /** \brief Fills the position of the segments (executable, read-only, read/write).
@@ -211,9 +207,8 @@ void find_object_address(
       // .bss is usually after the .data:
       simgrid::xbt::VmMap const& next = maps[i + 1];
       if (next.pathname.empty() && (next.prot & PROT_WRITE)
-          && next.start_addr == reg.end_addr) {
+          && next.start_addr == reg.end_addr)
         result->end_rw = (char*) maps[i + 1].end_addr;
-      }
     } else if ((reg.prot & PROT_READ) && (reg.prot & PROT_EXEC)) {
       xbt_assert(!result->start_exec,
                  "Multiple executable segments for %s, not supported",
@@ -300,9 +295,9 @@ static void fill_local_variables_values(mc_stack_frame_t stack_frame,
     new_var.region = region_type;
     new_var.address = nullptr;
 
-    if (current_variable.address != nullptr) {
+    if (current_variable.address != nullptr)
       new_var.address = current_variable.address;
-    else if (!current_variable.location_list.empty()) {
+    else if (!current_variable.location_list.empty()) {
       simgrid::dwarf::Location location =
         simgrid::dwarf::resolve(
           current_variable.location_list,
@@ -315,9 +310,8 @@ static void fill_local_variables_values(mc_stack_frame_t stack_frame,
         xbt_die("Cannot handle non-address variable");
       new_var.address = location.address();
 
-    } else {
+    } else
       xbt_die("No address");
-    }
 
     result.push_back(std::move(new_var));
   }
@@ -345,11 +339,9 @@ static std::vector<s_mc_stack_frame_t> unwind_stack_frames(mc_unw_context_t stac
   unw_cursor_t c;
 
   // TODO, check condition check (unw_init_local==0 means end of frame)
-  if (mc_unw_init_cursor(&c, stack_context) != 0) {
-
+  if (mc_unw_init_cursor(&c, stack_context) != 0)
     xbt_die("Could not initialize stack unwinding");
 
-  } else
     while (1) {
 
       s_mc_stack_frame_t stack_frame;
@@ -386,11 +378,10 @@ static std::vector<s_mc_stack_frame_t> unwind_stack_frames(mc_unw_context_t stac
         break;
 
       int ret = unw_step(&c);
-      if (ret == 0) {
+      if (ret == 0)
         xbt_die("Unexpected end of stack.");
-      } else if (ret < 0) {
+      else if (ret < 0)
         xbt_die("Error while unwinding stack");
-      }
     }
 
   if (result.empty()) {
@@ -414,9 +405,9 @@ static std::vector<s_mc_snapshot_stack_t> take_snapshot_stacks(mc_snapshot_t * s
       &context, sizeof(context), remote(stack.context));
 
     if (mc_unw_init_context(&st.context, &mc_model_checker->process(),
-      &context) < 0) {
+      &context) < 0)
       xbt_die("Could not initialise the libunwind context.");
-    }
+
     st.stack_frames = unwind_stack_frames(&st.context);
     st.local_variables = get_local_variables_values(st.stack_frames, stack.process_index);
     st.process_index = stack.process_index;
@@ -451,9 +442,8 @@ static void snapshot_handle_ignore(mc_snapshot_t snapshot)
   }
 
   // Zero the memory:
-  for(auto const& region : mc_model_checker->process().ignored_regions()) {
+  for(auto const& region : mc_model_checker->process().ignored_regions())
     snapshot->process()->clear_bytes(remote(region.addr), region.size);
-  }
 
 }
 
@@ -500,12 +490,12 @@ static std::vector<s_fd_infos_t> get_current_fds(pid_t pid)
     const size_t link_size = 200;
     char link[200];
     res = readlink(source, link, link_size);
-    if (res<0) {
+
+    if (res<0)
       xbt_die("Could not read link for %s", source);
-    }
-    if (res==200) {
+    if (res==200)
       xbt_die("Buffer to small for link of %s", source);
-    }
+
     link[res] = '\0';
 
 #ifdef HAVE_SMPI
@@ -574,14 +564,12 @@ mc_snapshot_t take_snapshot(int num_state)
   if (_sg_mc_visited > 0 || strcmp(_sg_mc_property_file, "")) {
     snapshot->stacks =
         take_snapshot_stacks(&snapshot);
-    if (_sg_mc_hash) {
+    if (_sg_mc_hash)
       snapshot->hash = simgrid::mc::hash(*snapshot);
-    } else {
+    else
       snapshot->hash = 0;
-    }
-  } else {
+  } else
     snapshot->hash = 0;
-  }
 
   snapshot_ignore_restore(snapshot);
   if (use_soft_dirty)
@@ -619,10 +607,9 @@ void restore_snapshot_fds(mc_snapshot_t snapshot)
   for (auto const& fd : snapshot->current_fds) {
     
     int new_fd = open(fd.filename.c_str(), fd.flags);
-    if (new_fd < 0) {
+    if (new_fd < 0)
       xbt_die("Could not reopen the file %s fo restoring the file descriptor",
         fd.filename.c_str());
-    }
     if (new_fd != fd.number) {
       dup2(new_fd, fd.number);
       close(new_fd);
index d499d1b..6233659 100644 (file)
@@ -54,9 +54,8 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t com
     if (!memcmp(comm1->data, comm2->data, comm1->data_size))
       return NONE_DIFF;
     return DATA_DIFF;
-  }else{
+  } else
     return DATA_DIFF;
-  }
   return NONE_DIFF;
 }
 
@@ -249,9 +248,8 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
     pattern->rdv = mc_model_checker->process().read_string(remote_name);
     pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
     pattern->dst_host = MC_smx_process_get_host_name(issuer);
-  } else {
+  } else
     xbt_die("Unexpected call_type %i", (int) call_type);
-  }
 
   xbt_dynar_push(
     xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t),
@@ -267,7 +265,7 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne
   int completed = 0;
 
   /* Complete comm pattern */
-  xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern) {
+  xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
     if (current_comm_pattern->comm_addr == comm_addr) {
       update_comm_pattern(current_comm_pattern, comm_addr);
       completed = 1;
@@ -277,17 +275,17 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne
       XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
       break;
     }
-  }
+
   if(!completed)
     xbt_die("Corresponding communication not found!");
 
   mc_list_comm_pattern_t pattern = xbt_dynar_get_as(
     initial_communications_pattern, issuer, mc_list_comm_pattern_t);
 
-  if (!initial_global_state->initial_communications_pattern_done) {
+  if (!initial_global_state->initial_communications_pattern_done)
     /* Store comm pattern */
     xbt_dynar_push(pattern->list, &comm_pattern);
-  else {
+  else {
     /* Evaluate comm determinism */
     deterministic_comm_pattern(issuer, comm_pattern, backtracking);
     pattern->index_comm++;
@@ -369,18 +367,16 @@ static int MC_modelcheck_comm_determinism_main(void)
       XBT_DEBUG("Execute: %s", req_str);
       xbt_free(req_str);
       
-      if (dot_output != nullptr) {
+      if (dot_output != nullptr)
         req_str = MC_request_get_dot_output(req, value);
-      }
 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
 
       /* TODO : handle test and testany simcalls */
       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
-      if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
+      if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
         call = MC_get_call_type(req);
-      }
 
       /* Answer the request */
       MC_simcall_handle(req, value);    /* After this call req is no longer useful */
@@ -406,12 +402,9 @@ static int MC_modelcheck_comm_determinism_main(void)
         if (dot_output != nullptr)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,  next_state->num, req_str);
 
-      } else {
-
-        if (dot_output != nullptr)
-          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
-
-      }
+      } else if (dot_output != nullptr)
+        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
+          state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 
       xbt_fifo_unshift(mc_stack, next_state);
 
@@ -420,13 +413,12 @@ static int MC_modelcheck_comm_determinism_main(void)
 
     } else {
 
-      if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) {
+      if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth)
         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
-      } else if (visited_state != nullptr) {
+      else if (visited_state != nullptr)
         XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
-      } else {
+      else
         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack));
-      }
 
       if (!initial_global_state->initial_communications_pattern_done) 
         initial_global_state->initial_communications_pattern_done = 1;
@@ -444,7 +436,7 @@ static int MC_modelcheck_comm_determinism_main(void)
         return SIMGRID_MC_EXIT_DEADLOCK;
       }
 
-      while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != nullptr) {
+      while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != nullptr)
         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
@@ -459,7 +451,7 @@ static int MC_modelcheck_comm_determinism_main(void)
           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
         }
-      }
+
     }
   }
 
@@ -473,10 +465,9 @@ int MC_modelcheck_comm_determinism(void)
   mc_reduce_kind = e_mc_reduce_none;
   mc_model_checker->wait_for_requests();
 
-  if (mc_mode == MC_MODE_CLIENT) {
+  if (mc_mode == MC_MODE_CLIENT)
     // This will move somehwere else:
     MC_client_handle_messages();
-  }
 
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
index 857bee8..0a5ff5e 100644 (file)
@@ -75,16 +75,14 @@ void MC_restore_communications_pattern(mc_state_t state)
   mc_list_comm_pattern_t list_process_comm;
   unsigned int cursor;
 
-  xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){
+  xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm)
     list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int);
-  }
 
-  for (unsigned i = 0; i < MC_smx_get_maxpid(); i++) {
+  for (unsigned i = 0; i < MC_smx_get_maxpid(); i++)
     MC_patterns_copy(
       xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t),
       xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t)
     );
-  }
 }
 
 void MC_state_copy_incomplete_communications_pattern(mc_state_t state)
@@ -103,9 +101,8 @@ void MC_state_copy_index_communications_pattern(mc_state_t state)
   state->index_comm = xbt_dynar_new(sizeof(unsigned int), nullptr);
   mc_list_comm_pattern_t list_process_comm;
   unsigned int cursor;
-  xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){
+  xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm)
     xbt_dynar_push_as(state->index_comm, unsigned int, list_process_comm->index_comm);
-  }
 }
 
 void MC_handle_comm_pattern(
index 00ead0e..634402e 100644 (file)
@@ -150,19 +150,17 @@ static int compare_areas_with_type(ComparisonState& state,
     void* addr_pointed1 = MC_region_read_pointer(region1, real_area1);
     void* addr_pointed2 = MC_region_read_pointer(region2, real_area2);
 
-    if (type->subtype && type->subtype->type == DW_TAG_subroutine_type) {
+    if (type->subtype && type->subtype->type == DW_TAG_subroutine_type)
       return (addr_pointed1 != addr_pointed2);
-    } else {
-
-      if (addr_pointed1 == nullptr && addr_pointed2 == NULL)
-        return 0;
-      if (addr_pointed1 == nullptr || addr_pointed2 == NULL)
-        return 1;
-      if (!state.compared_pointers.insert(
-          std::make_pair(addr_pointed1, addr_pointed2)).second)
-        return 0;
+    if (addr_pointed1 == nullptr && addr_pointed2 == NULL)
+      return 0;
+    if (addr_pointed1 == nullptr || addr_pointed2 == NULL)
+      return 1;
+    if (!state.compared_pointers.insert(
+        std::make_pair(addr_pointed1, addr_pointed2)).second)
+      return 0;
 
-      pointer_level++;
+    pointer_level++;
 
       // Some cases are not handled here:
       // * the pointers lead to different areas (one to the heap, the other to the RW segment ...);
@@ -186,21 +184,19 @@ static int compare_areas_with_type(ComparisonState& state,
           return 1;
         if (!type->type_id)
           return (addr_pointed1 != addr_pointed2);
-        else {
+        else
           return compare_areas_with_type(state, process_index,
                                          addr_pointed1, snapshot1, region1,
                                          addr_pointed2, snapshot2, region2,
                                          type->subtype, pointer_level);
-        }
       }
 
       // TODO, We do not handle very well the case where
       // it belongs to a different (non-heap) region from the current one.
 
-      else {
+      else
         return (addr_pointed1 != addr_pointed2);
-      }
-    }
+
     break;
   }
   case DW_TAG_structure_type:
@@ -243,9 +239,8 @@ static int compare_global_variables(simgrid::mc::ObjectInformation* object_info,
 #ifdef HAVE_SMPI
   if (r1->storage_type() == simgrid::mc::StorageType::Privatized) {
     xbt_assert(process_index >= 0);
-    if (r2->storage_type() != simgrid::mc::StorageType::Privatized) {
+    if (r2->storage_type() != simgrid::mc::StorageType::Privatized)
       return 1;
-    }
 
     size_t process_count = MC_smpi_process_count();
     xbt_assert(process_count == r1->privatized_data().size()
@@ -309,7 +304,8 @@ static int compare_local_variables(int process_index,
   if (stack1->local_variables.size() != stack2->local_variables.size()) {
     XBT_VERB("Different number of local variables");
     return 1;
-  } else {
+  }
+
     unsigned int cursor = 0;
     local_variable_t current_var1, current_var2;
     int res;
@@ -353,7 +349,6 @@ static int compare_local_variables(int process_index,
       cursor++;
     }
     return 0;
-  }
 }
 
 int snapshot_compare(void *state1, void *state2)
@@ -392,9 +387,8 @@ int snapshot_compare(void *state1, void *state2)
 #ifndef MC_DEBUG
       return 1;
 #endif
-    } else {
+    } else
       XBT_VERB("(%d - %d) Same hash : 0x%" PRIx64, num1, num2, s1->hash);
-    }
   }
 
   /* Compare enabled processes */
index cae5320..244b4a0 100644 (file)
@@ -38,10 +38,10 @@ int _sg_mc_timeout = 0;
 
 void _mc_cfg_cb_timeout(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !(_sg_do_model_check || MC_record_path)) {
+  if (_sg_cfg_init_status && !(_sg_do_model_check || MC_record_path))
     xbt_die
         ("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_timeout = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
@@ -66,34 +66,33 @@ int _sg_mc_termination = 0;
 
 void _mc_cfg_cb_reduce(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die
         ("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   char *val = xbt_cfg_get_string(_sg_cfg_set, name);
-  if (!strcasecmp(val, "none")) {
+  if (!strcasecmp(val, "none"))
     mc_reduce_kind = e_mc_reduce_none;
-  } else if (!strcasecmp(val, "dpor")) {
+  else if (!strcasecmp(val, "dpor"))
     mc_reduce_kind = e_mc_reduce_dpor;
-  } else {
+  else
     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",
             name);
-  }
 }
 
 void _mc_cfg_cb_checkpoint(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die
         ("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
@@ -103,6 +102,7 @@ void _mc_cfg_cb_soft_dirty(const char *name, int pos) {
             "(through MSG_config?), but model-checking was not activated "
             "at config time (through --cfg=model-check:1). "
             "This won't work, sorry.");
+
   _sg_mc_soft_dirty = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
@@ -110,87 +110,88 @@ void _mc_cfg_cb_ksm(const char *name, int pos)
 {
   if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die("You are specifying a KSM value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+
   _sg_mc_ksm = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_property(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die
         ("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_property_file = xbt_cfg_get_string(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_hash(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die
         ("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_hash = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_snapshot_fds(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die
         ("You are specifying a value to enable/disable the use of FD snapshoting, but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_snapshot_fds = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_max_depth(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die
         ("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_max_depth = xbt_cfg_get_int(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_visited(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die
         ("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_visited = xbt_cfg_get_int(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_dot_output(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die
         ("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_dot_output_file = xbt_cfg_get_string(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_comms_determinism(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die
         ("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_comms_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_send_determinism(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die
         ("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_termination(const char *name, int pos)
 {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check)
     xbt_die
         ("You are specifying a value to enable/disable the detection of non progressive cycles after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
-  }
+
   _sg_mc_termination = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
index 1490675..f7e1e8e 100644 (file)
@@ -86,12 +86,11 @@ static int is_new_heap_area_pair(xbt_dynar_t list, int block1, int fragment1,
   unsigned int cursor = 0;
   heap_area_pair_t current_pair;
 
-  xbt_dynar_foreach(list, cursor, current_pair) {
+  xbt_dynar_foreach(list, cursor, current_pair)
     if (current_pair->block1 == block1 && current_pair->block2 == block2
         && current_pair->fragment1 == fragment1
         && current_pair->fragment2 == fragment2)
       return 0;
-  }
 
   return 1;
 }
@@ -160,7 +159,7 @@ static void match_equals(struct s_mc_diff *state, xbt_dynar_t list)
   unsigned int cursor = 0;
   heap_area_pair_t current_pair;
 
-  xbt_dynar_foreach(list, cursor, current_pair) {
+  xbt_dynar_foreach(list, cursor, current_pair)
 
     if (current_pair->fragment1 != -1) {
 
@@ -178,7 +177,6 @@ static void match_equals(struct s_mc_diff *state, xbt_dynar_t list)
 
     }
 
-  }
 }
 
 /** Check whether two blocks are known to be matching
@@ -715,14 +713,12 @@ static int compare_heap_area_without_type(struct s_mc_diff *state, int process_i
         res_compare =
             compare_heap_area(process_index, addr_pointed1, addr_pointed2, snapshot1,
                               snapshot2, previous, nullptr, 0);
-        if (res_compare == 1) {
+        if (res_compare == 1)
           return res_compare;
-        }
         i = pointer_align + sizeof(void *);
         continue;
-      } else {
+      } else
         return 1;
-      }
 
     }
 
@@ -770,9 +766,8 @@ top:
       && ((ignore1 = heap_comparison_ignore_size(state->to_ignore1, real_area1))
           > 0)
       && ((ignore2 = heap_comparison_ignore_size(state->to_ignore2, real_area2))
-          == ignore1)) {
+          == ignore1))
     return 0;
-  }
 
   simgrid::mc::Type *subtype, *subsubtype;
   int res, elm_size;
@@ -794,9 +789,8 @@ top:
     } else {
       if (area_size != -1 && type->byte_size != area_size)
         return -1;
-      else {
+      else
         return (MC_snapshot_region_memcmp(real_area1, heap_region1, real_area2, heap_region2, type->byte_size) != 0);
-      }
     }
     break;
   case DW_TAG_enumeration_type:
@@ -917,9 +911,8 @@ top:
           if (res == 1)
             return res;
         }
-      } else {
+      } else
         return -1;
-      }
     } else {
       for(simgrid::mc::Member& member : type->members) {
         // TODO, optimize this? (for the offset case)
@@ -932,9 +925,8 @@ top:
                                         snapshot1, snapshot2,
                                         previous, member.type, -1,
                                         check_ignore, 0);
-        if (res == 1) {
+        if (res == 1)
           return res;
-        }
       }
     }
     break;
@@ -1075,9 +1067,8 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
       || (block1 > (ssize_t) state->heapsize1) || (block1 < 1)
       || ((char *) area2 < (char *) state->std_heap_copy.heapbase)
       || (block2 > (ssize_t) state->heapsize2) || (block2 < 1)) {
-    if (match_pairs) {
+    if (match_pairs)
       xbt_dynar_free(&previous);
-    }
     return 1;
   }
 
@@ -1158,17 +1149,15 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
 
     if (heapinfo1->busy_block.size !=
         heapinfo2->busy_block.size) {
-      if (match_pairs) {
+      if (match_pairs)
         xbt_dynar_free(&previous);
-      }
       return 1;
     }
 
     if (heapinfo1->busy_block.busy_size !=
         heapinfo2->busy_block.busy_size) {
-      if (match_pairs) {
+      if (match_pairs)
         xbt_dynar_free(&previous);
-      }
       return 1;
     }
 
@@ -1184,12 +1173,10 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
 
     // Remember (basic) type inference.
     // The current data structure only allows us to do this for the whole block.
-    if (type != nullptr && area1 == real_addr_block1) {
+    if (type != nullptr && area1 == real_addr_block1)
       state->types1_(block1, 0) = type;
-    }
-    if (type != nullptr && area2 == real_addr_block2) {
+    if (type != nullptr && area2 == real_addr_block2)
       state->types2_(block2, 0) = type;
-    }
 
     if (size <= 0) {
       if (match_pairs) {
@@ -1265,9 +1252,8 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
         }
         return -1;
       } else {
-        if (match_pairs) {
+        if (match_pairs)
           xbt_dynar_free(&previous);
-        }
         return 1;
       }
     }
@@ -1277,12 +1263,11 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
 
     // Remember (basic) type inference.
     // The current data structure only allows us to do this for the whole fragment.
-    if (type != nullptr && area1 == real_addr_frag1) {
+    if (type != nullptr && area1 == real_addr_frag1)
       state->types1_(block1, frag1) = type;
-    }
-    if (type != nullptr && area2 == real_addr_frag2) {
+    if (type != nullptr && area2 == real_addr_frag2)
       state->types2_(block2, frag2) = type;
-    }
+
     // The type of the variable is already known:
     if (type) {
       new_type1 = type;
@@ -1351,15 +1336,14 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
       size = new_size1;
     }
 
-    if (offset1 == 0 && offset2 == 0) {
-      if (!add_heap_area_pair(previous, block1, frag1, block2, frag2)) {
+    if (offset1 == 0 && offset2 == 0
+      && !add_heap_area_pair(previous, block1, frag1, block2, frag2)) {
         if (match_pairs) {
           match_equals(state, previous);
           xbt_dynar_free(&previous);
         }
         return 0;
       }
-    }
 
     if (size <= 0) {
       if (match_pairs) {
@@ -1376,25 +1360,24 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
 
   } else {
 
-    if (match_pairs) {
+    if (match_pairs)
       xbt_dynar_free(&previous);
-    }
     return 1;
 
   }
 
 
   /* Start comparison */
-  if (type) {
+  if (type)
     res_compare =
         compare_heap_area_with_type(state, process_index, area1, area2, snapshot1, snapshot2,
                                     previous, type, size, check_ignore,
                                     pointer_level);
-  } else {
+  else
     res_compare =
         compare_heap_area_without_type(state, process_index, area1, area2, snapshot1, snapshot2,
                                        previous, size, check_ignore);
-  }
+
   if (res_compare == 1) {
     if (match_pairs)
       xbt_dynar_free(&previous);
@@ -1439,13 +1422,13 @@ static int get_pointed_area_size(void *area, int heap)
 
   if (heapinfo[block].type == MMALLOC_TYPE_FREE || heapinfo[block].type == MMALLOC_TYPE_HEAPINFO) {     /* Free block */
     return -1;
-  } else if (heapinfo[block].type == MMALLOC_TYPE_UNFRAGMENTED) {       /* Complete block */
+  else if (heapinfo[block].type == MMALLOC_TYPE_UNFRAGMENTED)       /* Complete block */
     return (int) heapinfo[block].busy_block.busy_size;
-  } else {
+  else
     frag =
         ((uintptr_t) (ADDR2UINT(area) % (BLOCKSIZE))) >> heapinfo[block].type;
     return (int) heapinfo[block].busy_frag.frag_size[frag];
-  }
+
 }
 
 #ifndef max
index 38c7d3a..5e1b5e5 100644 (file)
@@ -257,11 +257,10 @@ static const char *MC_dwarf_attr_integrate_string(Dwarf_Die * die,
                                                   int attribute)
 {
   Dwarf_Attribute attr;
-  if (!dwarf_attr_integrate(die, attribute, &attr)) {
+  if (!dwarf_attr_integrate(die, attribute, &attr))
     return nullptr;
-  } else {
+  else
     return dwarf_formstring(&attr);
-  }
 }
 
 /** \brief Get the linkage name of a DIE.
@@ -867,9 +866,8 @@ static void MC_dwarf_handle_scope_die(simgrid::mc::ObjectInformation* info, Dwar
   if (low_pc) {
     // DW_AT_high_pc:
     Dwarf_Attribute attr;
-    if (!dwarf_attr_integrate(die, DW_AT_high_pc, &attr)) {
+    if (!dwarf_attr_integrate(die, DW_AT_high_pc, &attr))
       xbt_die("Missing DW_AT_high_pc matching with DW_AT_low_pc");
-    }
 
     Dwarf_Sword offset;
     Dwarf_Addr high_pc;
@@ -941,9 +939,8 @@ static void MC_dwarf_handle_children(simgrid::mc::ObjectInformation* info, Dwarf
   Dwarf_Die child;
   int res;
   for (res = dwarf_child(die, &child); res == 0;
-       res = dwarf_siblingof(&child, &child)) {
+       res = dwarf_siblingof(&child, &child))
     MC_dwarf_handle_die(info, &child, unit, frame, ns);
-  }
 }
 
 static void MC_dwarf_handle_die(simgrid::mc::ObjectInformation* info, Dwarf_Die * die,
@@ -1176,7 +1173,7 @@ void MC_post_process_object_info(simgrid::mc::Process* process, simgrid::mc::Obj
         break;
 
     // Resolve full_type:
-    if (!subtype->name.empty() && subtype->byte_size == 0) {
+    if (!subtype->name.empty() && subtype->byte_size == 0)
       for (auto const& object_info : process->object_infos) {
         auto i = object_info->full_types_by_name.find(subtype->name);
         if (i != object_info->full_types_by_name.end()
@@ -1185,7 +1182,7 @@ void MC_post_process_object_info(simgrid::mc::Process* process, simgrid::mc::Obj
           break;
         }
       }
-    else type->full_type = subtype;
+    else type->full_type = subtype;
 
   }
 }
index 1fc984e..a77c614 100644 (file)
@@ -112,9 +112,8 @@ void MC_init()
     MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
 
     smx_process_t process;
-    xbt_swag_foreach(process, simix_global->process_list) {
+    xbt_swag_foreach(process, simix_global->process_list)
       MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
-    }
   }
 }
 
@@ -149,28 +148,25 @@ int MC_deadlock_check()
     ssize_t s = mc_model_checker->process().receive_message(message);
     if (s == -1)
       xbt_die("Could not receive message");
-    else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) {
+    if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
       xbt_die("%s received unexpected message %s (%i, size=%i) "
         "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
         MC_mode_name(mc_mode),
         MC_message_type_name(message.type), (int) message.type, (int) s,
         (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
         );
-    }
-    else
-      return message.value;
+    return message.value;
   }
 
   int deadlock = FALSE;
   smx_process_t process;
   if (xbt_swag_size(simix_global->process_list)) {
     deadlock = TRUE;
-    xbt_swag_foreach(process, simix_global->process_list) {
+    xbt_swag_foreach(process, simix_global->process_list)
       if (MC_process_is_enabled(process)) {
         deadlock = FALSE;
         break;
       }
-    }
   }
   return deadlock;
 }
@@ -509,14 +505,11 @@ static void MC_dump_stacks(FILE* file)
 
 double MC_process_clock_get(smx_process_t process)
 {
-  if (mc_time) {
-    if (process != nullptr)
-      return mc_time[process->pid];
-    else
-      return -1;
-  } else {
+  if (!mc_time)
     return 0;
-  }
+  if (process != nullptr)
+    return mc_time[process->pid];
+  return -1;
 }
 
 void MC_process_clock_add(smx_process_t process, double amount)
index 5a440b5..1df9b1a 100644 (file)
@@ -92,9 +92,9 @@ void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* cont
       ((char *) stack -
        (char *) heap->heapbase) / BLOCKSIZE + 1;
 #ifdef HAVE_SMPI
-  if (smpi_privatize_global_variables && process) {
+  if (smpi_privatize_global_variables && process)
     region.process_index = smpi_process_index_of_smx_process(process);
-  else
+  else
 #endif
   region.process_index = -1;
 
index d184f90..3d9dd53 100644 (file)
@@ -57,11 +57,9 @@ static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair)
   new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
   new_pair->acceptance_pair = 1;
 
-  if (xbt_dynar_is_empty(acceptance_pairs)) {
-
+  if (xbt_dynar_is_empty(acceptance_pairs))
     xbt_dynar_push(acceptance_pairs, &new_pair);
-
-  } else {
+  else {
 
     int min = -1, max = -1, index;
     //int res;
@@ -99,14 +97,12 @@ static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair)
       xbt_dynar_insert_at(acceptance_pairs, min, &new_pair);
     } else {
       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t);
-      if (pair_test->nb_processes < new_pair->nb_processes) {
+      if (pair_test->nb_processes < new_pair->nb_processes)
         xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
-      } else {
-        if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
-          xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
-        else
-          xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
-      }
+      else if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
+        xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
+      else
+        xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
     }
   }
   return new_pair;
@@ -118,12 +114,11 @@ static void remove_acceptance_pair(int pair_num)
   mc_visited_pair_t pair_test = nullptr;
   int pair_found = 0;
 
-  xbt_dynar_foreach(acceptance_pairs, cursor, pair_test) {
+  xbt_dynar_foreach(acceptance_pairs, cursor, pair_test)
     if (pair_test->num == pair_num) {
        pair_found = 1;
       break;
     }
-  }
 
   if(pair_found == 1) {
     xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
@@ -165,9 +160,8 @@ static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
       }
       return -1;
     }
-  case 4:{
-      return 2;
-    }
+  case 4:
+    return 2;
   default:
     return -1;
   }
index 3df9bbe..5a452f6 100644 (file)
@@ -21,9 +21,8 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory, mc,
 /* It creates the two heap regions: std_heap and mc_heap */
 void MC_memory_init()
 {
-  if (!malloc_use_mmalloc()) {
+  if (!malloc_use_mmalloc())
     xbt_die("Model-checking support is not enabled: run with simgrid-mc.");
-  }
 }
 
 /* Finalize the memory subsystem */
index 50b83dd..1117208 100644 (file)
@@ -27,9 +27,8 @@ static inline __attribute__ ((always_inline))
 size_t mc_page_count(size_t size)
 {
   size_t page_count = size >> xbt_pagebits;
-  if (size & (xbt_pagesize-1)) {
+  if (size & (xbt_pagesize-1))
     page_count ++;
-  }
   return page_count;
 }
 
index 29fd979..027bdda 100644 (file)
@@ -27,12 +27,11 @@ int MC_protocol_send(int socket, const void* message, std::size_t size)
     MC_mode_name(mc_mode),
     MC_message_type_name(*(e_mc_message_type*) message));
 
-  while (send(socket, message, size, 0) == -1) {
+  while (send(socket, message, size, 0) == -1)
     if (errno == EINTR)
       continue;
     else
       return errno;
-  }
   return 0;
 }
 
@@ -46,11 +45,10 @@ int MC_protocol_send_simple_message(int socket, e_mc_message_type type)
 ssize_t MC_receive_message(int socket, void* message, size_t size, int options)
 {
   int res = recv(socket, message, size, options);
-  if (res != -1) {
+  if (res != -1)
     XBT_DEBUG("Protocol [%s] received %s",
       MC_mode_name(mc_mode),
       MC_message_type_name(*(e_mc_message_type*) message));
-  }
   return res;
 }
 
index 0e8640d..f85fad2 100644 (file)
@@ -348,9 +348,8 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
       args = bprintf("comm=%s (%d of %lu)",
         p, value + 1, xbt_dynar_length(&comms));
       xbt_free(p);
-    } else {
+    } else
       args = bprintf("comm at idx %d", value);
-    }
     break;
   }
 
@@ -412,19 +411,18 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
   }
 
   char* str;
-  if (args != nullptr) {
+  if (args != nullptr)
     str =
         bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
                 MC_smx_process_get_host_name(issuer),
                 MC_smx_process_get_name(issuer),
                 type, args);
-  } else {
+  else
     str =
         bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
                 MC_smx_process_get_host_name(issuer),
                 MC_smx_process_get_name(issuer),
                 type);
-  }
   xbt_free(args);
   return str;
 }
index 5d3c23a..4047f13 100644 (file)
@@ -112,9 +112,8 @@ int MC_modelcheck_safety(void)
       XBT_DEBUG("Execute: %s", req_str);
       xbt_free(req_str);
 
-      if (dot_output != nullptr) {
+      if (dot_output != nullptr)
         req_str = MC_request_get_dot_output(req, value);
-      }
 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
@@ -147,12 +146,9 @@ int MC_modelcheck_safety(void)
         if (dot_output != nullptr)
           std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 
-      } else {
-
-        if (dot_output != nullptr)
-          std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
+      } else if (dot_output != nullptr)
+        std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 
-      }
 
       xbt_fifo_unshift(mc_stack, next_state);
 
@@ -173,12 +169,9 @@ int MC_modelcheck_safety(void)
         else
           XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
 
-      } else {
-
+      } else
         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
 
-      }
-
       /* Trash the current state, no longer needed */
       xbt_fifo_shift(mc_stack);
       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
index 409834a..07f11b8 100644 (file)
@@ -212,12 +212,10 @@ int MC_smpi_process_count(void)
 {
   if (mc_mode == MC_MODE_CLIENT)
     return smpi_process_count();
-  else {
-    int res;
-    mc_model_checker->process().read_variable("process_count",
-      &res, sizeof(res));
-    return res;
-  }
+  int res;
+  mc_model_checker->process().read_variable("process_count",
+    &res, sizeof(res));
+  return res;
 }
 #endif
 
index d39fbf7..eb9e92d 100644 (file)
@@ -41,15 +41,12 @@ mc_mem_region_t mc_get_snapshot_region(
     if (region->storage_type() == simgrid::mc::StorageType::Privatized) {
 #ifdef HAVE_SMPI
       // Use the current process index of the snapshot:
-      if (process_index == simgrid::mc::ProcessIndexDisabled) {
+      if (process_index == simgrid::mc::ProcessIndexDisabled)
         process_index = snapshot->privatization_index;
-      }
-      if (process_index < 0) {
+      if (process_index < 0)
         xbt_die("Missing process index");
-      }
-      if (process_index >= (int) region->privatized_data().size()) {
+      if (process_index >= (int) region->privatized_data().size())
         xbt_die("Invalid process index");
-      }
       simgrid::mc::RegionSnapshot& priv_region = region->privatized_data()[process_index];
       xbt_assert(priv_region.contain(simgrid::mc::remote(addr)));
       return &priv_region;
@@ -82,9 +79,8 @@ const void* MC_region_read_fragmented(mc_mem_region_t region, void* target, cons
 
   void* dest = target;
 
-  if (dest==nullptr) {
+  if (dest==nullptr)
     xbt_die("Missing destination buffer for fragmented memory access");
-  }
 
   // Read each page:
   while (mc_page_number(nullptr, addr) != page_end) {
@@ -127,11 +123,10 @@ int MC_snapshot_region_memcmp(
   const void* buffer1 = MC_region_read(region1, buffer1a, addr1, size);
   const void* buffer2 = MC_region_read(region2, buffer2a, addr2, size);
   int res;
-  if (buffer1 == buffer2) {
+  if (buffer1 == buffer2)
     res = 0;
-  } else {
+  else
     res = memcmp(buffer1, buffer2, size);
-  }
   if (!stack_alloc) {
     free(buffer1a);
     free(buffer2a);
index 726294f..566d98d 100644 (file)
@@ -54,9 +54,8 @@ mc_state_t MC_state_new()
  * \param trans The state to be deleted
  */
 void MC_state_delete(mc_state_t state, int free_snapshot){
-  if (state->system_state && free_snapshot){
+  if (state->system_state && free_snapshot)
     delete state->system_state;
-  }
   if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
     xbt_free(state->index_comm);
     xbt_free(state->incomplete_comm_pattern);
@@ -81,13 +80,10 @@ void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process)
 unsigned int MC_state_interleave_size(mc_state_t state)
 {
   unsigned int i, size = 0;
-
-  for (i = 0; i < state->max_pid; i++) {
+  for (i = 0; i < state->max_pid; i++)
     if ((state->proc_status[i].state == MC_INTERLEAVE)
         || (state->proc_status[i].state == MC_MORE_INTERLEAVE))
       size++;
-  }
-
   return size;
 }
 
@@ -154,7 +150,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
   case SIMCALL_MC_RANDOM: {
     state->internal_req = *req;
     int random_max = simcall_mc_random__get__max(req);
-    if (value != random_max) {
+    if (value != random_max)
       for (auto& p : mc_model_checker->process().simix_processes()) {
         mc_procstate_t procstate = &state->proc_status[p.copy.pid];
         const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
@@ -163,7 +159,6 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
           break;
         }
       }
-    }
     break;
   }
 
@@ -224,13 +219,12 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         *value = -1;
         while (procstate->interleave_count <
                 read_length(mc_model_checker->process(),
-                  remote(simcall_comm_testany__get__comms(&process->simcall)))) {
+                  remote(simcall_comm_testany__get__comms(&process->simcall))))
           if (MC_request_is_enabled_by_idx
               (&process->simcall, procstate->interleave_count++)) {
             *value = procstate->interleave_count - 1;
             break;
           }
-        }
 
         if (procstate->interleave_count >=
             read_length(mc_model_checker->process(),
@@ -248,15 +242,13 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         s_smx_synchro_t act;
         mc_model_checker->process().read_bytes(
           &act, sizeof(act), remote(remote_act));
-        if (act.comm.src_proc && act.comm.dst_proc) {
+        if (act.comm.src_proc && act.comm.dst_proc)
           *value = 0;
-        } else {
-          if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
+        else if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
               && act.comm.detached == 1)
-            *value = 0;
-          else
-            *value = -1;
-        }
+          *value = 0;
+        else
+          *value = -1;
         procstate->state = MC_DONE;
         return &process->simcall;
       }
@@ -264,10 +256,8 @@ static inline smx_simcall_t MC_state_get_request_for_process(
       case SIMCALL_MC_RANDOM:
         if (procstate->state == MC_INTERLEAVE)
           *value = simcall_mc_random__get__min(&process->simcall);
-        else {
-          if (state->req_num < simcall_mc_random__get__max(&process->simcall))
-            *value = state->req_num + 1;
-        }
+        else if (state->req_num < simcall_mc_random__get__max(&process->simcall))
+          *value = state->req_num + 1;
         procstate->state = MC_DONE;
         return &process->simcall;
 
index 8f07b4c..38f0cbf 100644 (file)
@@ -42,11 +42,11 @@ static int is_exploration_stack_state(mc_visited_state_t state){
 
 void visited_state_free(mc_visited_state_t state)
 {
-  if (state) {
-    if(!is_exploration_stack_state(state))
-      delete state->system_state;
-    xbt_free(state);
-  }
+  if (!state)
+    return;
+  if(!is_exploration_stack_state(state))
+    delete state->system_state;
+  xbt_free(state);
 }
 
 void visited_state_free_voidp(void *s)
@@ -172,16 +172,15 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
     }
-    if (nb_processes_test < nb_processes) {
+    if (nb_processes_test < nb_processes)
       start = cursor + 1;
-    } else if (nb_processes_test > nb_processes) {
+    else if (nb_processes_test > nb_processes)
       end = cursor - 1;
-    } else {
-      if (heap_bytes_used_test < heap_bytes_used) {
-        start = cursor + 1;
-      } else if (heap_bytes_used_test > heap_bytes_used) {
-        end = cursor - 1;
-      } else {
+    else if (heap_bytes_used_test < heap_bytes_used)
+      start = cursor + 1;
+    else if (heap_bytes_used_test > heap_bytes_used)
+      end = cursor - 1;
+    else {
         *min = *max = cursor;
         previous_cursor = cursor - 1;
         while (previous_cursor >= 0) {
@@ -216,7 +215,6 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
           next_cursor++;
         }
         return -1;
-      }
     }
   }
   return cursor;
@@ -268,7 +266,6 @@ bool some_dommunications_are_not_finished()
 
 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 {
-
   if (_sg_mc_visited == 0)
     return nullptr;
 
@@ -284,11 +281,9 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 
   if (xbt_dynar_is_empty(visited_states)) {
-
     xbt_dynar_push(visited_states, &new_state);
     return nullptr;
-
-  } else {
+  }
 
     int min = -1, max = -1, index;
 
@@ -336,21 +331,21 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
 
       // The state has not been visited: insert the state in the dynamic array.
       mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
-      if (state_test->nb_processes < new_state->nb_processes) {
+      if (state_test->nb_processes < new_state->nb_processes)
         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
-      } else {
-        if (state_test->heap_bytes_used < new_state->heap_bytes_used)
-          xbt_dynar_insert_at(visited_states, index + 1, &new_state);
-        else
-          xbt_dynar_insert_at(visited_states, index, &new_state);
-      }
+      else if (state_test->heap_bytes_used < new_state->heap_bytes_used)
+        xbt_dynar_insert_at(visited_states, index + 1, &new_state);
+      else
+        xbt_dynar_insert_at(visited_states, index, &new_state);
 
        XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 
     }
 
-    // We have reached the maximum number of stored states;
-    if ((ssize_t) xbt_dynar_length(visited_states) > _sg_mc_visited) {
+  if ((ssize_t) xbt_dynar_length(visited_states) <= _sg_mc_visited)
+    return nullptr;
+
+  // We have reached the maximum number of stored states;
 
       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
 
@@ -360,21 +355,18 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
       unsigned int index2 = 0;
 
       mc_visited_state_t state_test;
-      xbt_dynar_foreach(visited_states, cursor2, state_test){
+      xbt_dynar_foreach(visited_states, cursor2, state_test)
         if (!mc_model_checker->is_important_snapshot(*state_test->system_state)
             && state_test->num < min2) {
           index2 = cursor2;
           min2 = state_test->num;
         }
-      }
 
       // and drop it:
       xbt_dynar_remove_at(visited_states, index2, nullptr);
       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
-    }
 
     return nullptr;
-  }
 }
 
 /**
@@ -386,18 +378,15 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
     return -1;
 
   mc_visited_pair_t new_visited_pair = nullptr;
-
-  if (visited_pair == nullptr) {
+  if (visited_pair == nullptr)
     new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
-  } else {
+  else
     new_visited_pair = visited_pair;
-  }
 
   if (xbt_dynar_is_empty(visited_pairs)) {
-
     xbt_dynar_push(visited_pairs, &new_visited_pair);
-
-  } else {
+    return -1;
+  }
 
     int min = -1, max = -1, index;
     //int res;
@@ -449,12 +438,9 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
               xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
               xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
               pair_test->visited_removed = 1;
-              if (pair_test->acceptance_pair) {
-                if (pair_test->acceptance_removed == 1)
-                  MC_visited_pair_delete(pair_test);
-              } else {
+              if (!pair_test->acceptance_pair
+                  || pair_test->acceptance_removed == 1)
                 MC_visited_pair_delete(pair_test);
-              }
               return new_visited_pair->other_num;
             }
           }
@@ -464,14 +450,12 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
       xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
     } else {
       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
-      if (pair_test->nb_processes < new_visited_pair->nb_processes) {
+      if (pair_test->nb_processes < new_visited_pair->nb_processes)
         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
-      } else {
-        if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
-          xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
-        else
-          xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
-      }
+      else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
+        xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
+      else
+        xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
     }
 
     if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
@@ -487,15 +471,9 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
       }
       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
       pair_test->visited_removed = 1;
-      if (pair_test->acceptance_pair) {
-        if (pair_test->acceptance_removed)
-          MC_visited_pair_delete(pair_test);
-      } else {
+      if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
         MC_visited_pair_delete(pair_test);
-      }
     }
-
-  }
   return -1;
 }