model-checker : ignore coverage variables

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 116e5db..15040a9 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -56,8 +56,12 @@ static size_t data_bss_ignore_size(void *address){
     var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
     if(var->address == address)
       return var->size;
-    if(var->address < address)
-      start = cursor + 1;
+    if(var->address < address){
+      if((void *)((char *)var->address + var->size) > address)
+        return (char *)var->address + var->size - (char*)address;
+      else
+        start = cursor + 1;
+    }
     if(var->address > address)
       end = cursor - 1;   
   }
@@ -67,12 +71,19 @@ static size_t data_bss_ignore_size(void *address){
 
 static int data_bss_program_region_compare(void *d1, void *d2, size_t size){
 
-  size_t i = 0;
+  size_t i = 0, ignore_size = 0;
   int pointer_align;
   void *addr_pointed1 = NULL, *addr_pointed2 = NULL;
   
   for(i=0; i<size; i++){
     if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
+      if((ignore_size = data_bss_ignore_size((char *)start_data_binary+i)) > 0){
+        i = i + ignore_size;
+        continue;
+      }else if((ignore_size = data_bss_ignore_size((char *)start_bss_binary+i)) > 0){
+        i = i + ignore_size;
+        continue;
+      }
       pointer_align = (i / sizeof(void*)) * sizeof(void*);
       addr_pointed1 = *((void **)((char *)d1 + pointer_align));
       addr_pointed2 = *((void **)((char *)d2 + pointer_align));

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index edc9339..4dfb227 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -115,6 +115,7 @@ xbt_automaton_t _mc_property_automaton = NULL;
 static void MC_assert_pair(int prop);
 static dw_location_t get_location(xbt_dict_t location_list, char *expr);
 static dw_frame_t get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset);
+static void ignore_coverage_variables(char *executable, int region_type);
 
 void MC_do_the_modelcheck_for_real() {
   if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') {
@@ -170,14 +171,17 @@ void MC_init(){
   xbt_dict_t libsimgrid_location_list = MC_get_location_list(ls_path);
   MC_get_local_variables(ls_path, libsimgrid_location_list, &mc_local_variables);
 
-  MC_UNSET_RAW_MEM;
-
   MC_init_memory_map_info();
 
   /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
   get_libsimgrid_plt_section();
   get_binary_plt_section();
 
+  ignore_coverage_variables(libsimgrid_path, 1);
+  ignore_coverage_variables(xbt_binary_name, 2);
+
+  MC_UNSET_RAW_MEM;
+
    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
   MC_ignore_stack("e", "*");
   MC_ignore_stack("__ex_cleanup", "*");
@@ -719,6 +723,70 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
 
 /************ MC_ignore ***********/ 
 
+static void ignore_coverage_variables(char *executable, int region_type){
+
+  FILE *fp;
+
+  char *command = bprintf("objdump --syms %s", executable);
+
+  fp = popen(command, "r");
+
+  if(fp == NULL){
+    perror("popen failed");
+    xbt_abort();
+  }
+
+  char *line = NULL;
+  ssize_t read;
+  size_t n = 0;
+
+  xbt_dynar_t line_tokens = NULL;
+  unsigned long int size, offset;
+  void *address;
+
+  while ((read = getline(&line, &n, fp)) != -1){
+
+    if(n == 0)
+      continue;
+
+     /* Wipeout the new line character */
+    line[read - 1] = '\0';
+
+    xbt_str_strip_spaces(line);
+    xbt_str_ltrim(line, NULL);
+
+    line_tokens = xbt_str_split(line, NULL);
+
+    if(xbt_dynar_length(line_tokens) < 3 || strcmp(xbt_dynar_get_as(line_tokens, 0, char *), "SYMBOL") == 0)
+      continue;
+
+    if(((strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char *), "gcov", 4) == 0)
+        || (strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char *), "__gcov", 6) == 0))
+       && (((strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 3, char *), ".bss") == 0) 
+            || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 3, char *), ".data") == 0)))){
+      if(region_type == 1){ /* libsimgrid */
+        offset = strtoul(xbt_dynar_get_as(line_tokens, 0, char*), NULL, 16);
+        size = strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char *), NULL, 16);
+        //XBT_DEBUG("Add ignore at address %p (size %lu)", (char *)start_text_libsimgrid+offset, size);
+        MC_ignore_data_bss((char *)start_text_libsimgrid+offset, size);
+      }else{ /* binary */
+        address = (void *)strtoul(xbt_dynar_get_as(line_tokens, 0, char*), NULL, 16);
+        size = strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char *), NULL, 16);
+        //XBT_DEBUG("Add ignore at address %p (size %lu)", address, size);
+        MC_ignore_data_bss(address, size);
+      }
+    }
+
+    xbt_dynar_free(&line_tokens);
+
+  }
+
+  free(command);
+  free(line);
+  pclose(fp);
+
+}
+
 void MC_ignore_heap(void *address, size_t size){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 92f7d93..cc11df9 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -194,6 +194,16 @@ void get_binary_plt_section(void);
 
 extern void *start_data_libsimgrid;
 extern void *end_raw_heap;
+extern void *start_data_binary;
+extern void *start_bss_binary;
+extern char *libsimgrid_path;
+extern void *start_text_libsimgrid;
+extern void *start_bss_libsimgrid;
+extern void *start_plt_libsimgrid;
+extern void *end_plt_libsimgrid;
+extern void *start_plt_binary;
+extern void *end_plt_binary;
+
 
 /********************************** DPOR for safety  **************************************/
 typedef enum {
@@ -217,13 +227,9 @@ extern xbt_fifo_t mc_stack_liveness;
 extern mc_global_t initial_state_liveness;
 extern xbt_automaton_t _mc_property_automaton;
 extern int compare;
-extern void *start_plt_libsimgrid;
-extern void *end_plt_libsimgrid;
-extern void *start_plt_binary;
-extern void *end_plt_binary;
 extern xbt_dynar_t mc_stack_comparison_ignore;
 extern xbt_dynar_t mc_data_bss_comparison_ignore;
-extern void *start_bss_libsimgrid;
+
 
 typedef struct s_mc_pair{
   mc_snapshot_t system_state;