[mc] Try to DRY in MC main loops

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index 1555981..5deb972 100644 (file)
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -337,17 +337,13 @@ void MC_modelcheck_comm_determinism(void)
         && (req = MC_state_get_request(state, &value))
         && (visited_state == NULL)) {
 
         && (req = MC_state_get_request(state, &value))
         && (visited_state == NULL)) {
 

-      /* Debug information */
-      if (XBT_LOG_ISENABLED(mc_comm_determinism, xbt_log_priority_debug)) {
-        req_str = MC_request_to_string(req, value);
-        XBT_DEBUG("Execute: %s", req_str);
-        xbt_free(req_str);
-      }
+      MC_LOG_REQUEST(mc_comm_determinism, req, value);

 
 

-      MC_SET_MC_HEAP;
-      if (dot_output != NULL)
+      if (dot_output != NULL) {
+        MC_SET_MC_HEAP;

         req_str = MC_request_get_dot_output(req, value);
         req_str = MC_request_get_dot_output(req, value);

-      MC_SET_STD_HEAP;
+        MC_SET_STD_HEAP;
+      }

 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 15e552a..aa2c992 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -252,7 +252,7 @@ void MC_pre_modelcheck_liveness(void)
       initial_pair->search_cycle = 0;
 
       xbt_fifo_unshift(mc_stack, initial_pair);
       initial_pair->search_cycle = 0;
 
       xbt_fifo_unshift(mc_stack, initial_pair);

-
+      

       MC_SET_STD_HEAP;
 
       MC_modelcheck_liveness();
       MC_SET_STD_HEAP;
 
       MC_modelcheck_liveness();


@@ -298,7 +298,6 @@ void MC_modelcheck_liveness()
 
   int value;
   smx_simcall_t req = NULL;
 
   int value;
   smx_simcall_t req = NULL;

-  char *req_str;

 
   xbt_automaton_transition_t transition_succ;
   unsigned int cursor = 0;
 
   xbt_automaton_transition_t transition_succ;
   unsigned int cursor = 0;


@@ -370,12 +369,7 @@ void MC_modelcheck_liveness()
           }
           MC_SET_STD_HEAP;
 
           }
           MC_SET_STD_HEAP;
 

-          /* Debug information */
-          if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) {
-            req_str = MC_request_to_string(req, value);
-            XBT_DEBUG("Execute: %s", req_str);
-            xbt_free(req_str);
-          }
+          MC_LOG_REQUEST(mc_liveness, req, value);

 
           MC_SET_MC_HEAP;
           if (dot_output != NULL) {
 
           MC_SET_MC_HEAP;
           if (dot_output != NULL) {

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index cac81a8..8911c14 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -854,6 +854,13 @@ void* mc_snapshot_read_pointer_region(void* addr, mc_mem_region_t region)
   return *(void**) mc_snapshot_read_region(addr, region, &res, sizeof(void*));
 }
 
   return *(void**) mc_snapshot_read_region(addr, region, &res, sizeof(void*));
 }
 

+#define MC_LOG_REQUEST(log, req, value) \
+  if (XBT_LOG_ISENABLED(log, xbt_log_priority_debug)) { \
+    char* req_str = MC_request_to_string(req, value); \
+    XBT_DEBUG("Execute: %s", req_str); \
+    xbt_free(req_str); \
+  }
+

 SG_END_DECL()
 
 #endif
 SG_END_DECL()
 
 #endif

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index 7807097..2a1df9b 100644 (file)
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -117,17 +117,13 @@ void MC_modelcheck_safety(void)
     if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
         && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
 
     if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
         && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
 

-      /* Debug information */
-      if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
-        req_str = MC_request_to_string(req, value);
-        XBT_DEBUG("Execute: %s", req_str);
-        xbt_free(req_str);
-      }
+      MC_LOG_REQUEST(mc_safety, req, value);

 
 

-      MC_SET_MC_HEAP;
-      if (dot_output != NULL)
+      if (dot_output != NULL) {
+        MC_SET_MC_HEAP;

         req_str = MC_request_get_dot_output(req, value);
         req_str = MC_request_get_dot_output(req, value);

-      MC_SET_STD_HEAP;
+        MC_SET_STD_HEAP;
+      }

 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;