[mc] Simplify the control flow

diff --git a/src/mc/Process.cpp b/src/mc/Process.cpp
index 5360933..5f52f50 100644 (file)
--- a/src/mc/Process.cpp
+++ b/src/mc/Process.cpp
@@ -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;
       count  -= res;
       buffer += res;
       offset += res;

-    } else if (res==0) {
+    } else if (res==0)

       return -1;
       return -1;

-    } else if (errno != EINTR) {
+    else if (errno != EINTR) {

       perror("pread_whole");
       return -1;
     }
       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;
       count  -= res;
       buffer += res;
       offset += res;

-    } else if (res==0) {
+    } else if (res==0)

       return -1;
       return -1;

-    } else if (errno != EINTR) {
+    else if (errno != EINTR)

       return -1;
       return -1;

-    }

   }
   return real_count;
 }
   }
   return real_count;
 }


@@ -389,34 +388,28 @@ void Process::init_memory_map_info()
 
 std::shared_ptr<simgrid::mc::ObjectInformation> Process::find_object_info(RemotePtr<void> addr) const
 {
 
 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
     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 object_info;

-    }
-  }

   return nullptr;
 }
 
 std::shared_ptr<ObjectInformation> Process::find_object_info_exec(RemotePtr<void> addr) const
 {
   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
     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 info;

-    }
-  }

   return nullptr;
 }
 
 std::shared_ptr<ObjectInformation> Process::find_object_info_rw(RemotePtr<void> addr) const
 {
   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
     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 info;

-    }
-  }

   return nullptr;
 }
 
   return nullptr;
 }
 


@@ -589,16 +582,14 @@ void Process::ignore_region(std::uint64_t addr, std::size_t size)
 
   std::size_t position;
   if (current_region->addr == addr) {
 
   std::size_t position;
   if (current_region->addr == addr) {

-    if (current_region->size < size) {
+    if (current_region->size < size)

       position = cursor + 1;
       position = cursor + 1;

-    } else {
+    else

       position = cursor;
       position = cursor;

-    }
-  } else if (current_region->addr < addr) {
+  } else if (current_region->addr < addr)

     position = cursor + 1;
     position = cursor + 1;

-  } else {
+  else

     position = cursor;
     position = cursor;

-  }

   ignored_regions_.insert(
     ignored_regions_.begin() + position, region);
 }
   ignored_regions_.insert(
     ignored_regions_.begin() + position, region);
 }

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index e8f1bb4..9717dfc 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -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;
        * 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);
           && 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: {
     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;
       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);
       comms = simcall_comm_waitany__get__comms(req);

-    }
+

     // Read all the dynar buffer:
     char buffer[buffer_size];
     if (mc_mode == MC_MODE_SERVER)
     // 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)
 {
 
 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 prng_random(min, max);

-  }
-

   return simcall->mc_value;
 }
 
   return simcall->mc_value;
 }
 

diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index 8f07b4c..38f0cbf 100644 (file)
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -42,11 +42,11 @@ static int is_exploration_stack_state(mc_visited_state_t state){
 
 void visited_state_free(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)
 }
 
 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;
     }
       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;
       start = cursor + 1;

-    } else if (nb_processes_test > nb_processes) {
+    else if (nb_processes_test > nb_processes)

       end = cursor - 1;
       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) {
         *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;
           next_cursor++;
         }
         return -1;

-      }

     }
   }
   return cursor;
     }
   }
   return cursor;


@@ -268,7 +266,6 @@ bool some_dommunications_are_not_finished()
 
 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 {
 
 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 {

-

   if (_sg_mc_visited == 0)
     return nullptr;
 
   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_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;
     xbt_dynar_push(visited_states, &new_state);
     return nullptr;

-
-  } else {
+  }

 
     int min = -1, max = -1, index;
 
 
     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);
 
       // 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);
         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));
 
     }
 
 
        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)");
 
 
       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;
       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;
         }
         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)");
 
       // and drop it:
       xbt_dynar_remove_at(visited_states, index2, nullptr);
       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");

-    }

 
     return nullptr;
 
     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;
     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);
     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;
     new_visited_pair = visited_pair;

-  }

 
   if (xbt_dynar_is_empty(visited_pairs)) {
 
   if (xbt_dynar_is_empty(visited_pairs)) {

-

     xbt_dynar_push(visited_pairs, &new_visited_pair);
     xbt_dynar_push(visited_pairs, &new_visited_pair);

-
-  } else {
+    return -1;
+  }

 
     int min = -1, max = -1, index;
     //int res;
 
     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;
               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);
                 MC_visited_pair_delete(pair_test);

-              }

               return new_visited_pair->other_num;
             }
           }
               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);
       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);
         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) {
     }
 
     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;
       }
       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);
         MC_visited_pair_delete(pair_test);

-      }

     }
     }

-
-  }

   return -1;
 }
 
   return -1;
 }