[mc] Do not try to handle scopes inside a subprogram

The variables of a subprogram scopes were merged in the information
about subprogram without any information on its range of validity (for
which range of IP the variable is valid).

As this handling of scopes was broken, this commit ignore the scopes within a
subprogram.

We need to:

  * either add frame_t as child of frame_t to represent scope;

  * or attach validity information on each variables

    This one is needed anyway in order to handle DW_AT_start_scope.

  * or both.

    Use frame_t for DW_TAG_inlined_subprogram and validity range for
    real scope.

-    if(dwarf_offdie(dwarf, offset+length, &die)!=NULL) {
-      MC_dwarf_handle_die(info, &die, &die, NULL);
+    if(dwarf_offdie(dwarf, offset+length, &unit_die)!=NULL) {
+      Dwarf_Die child;
+      int res;
+      for (res=dwarf_child(&unit_die, &child); res==0; res=dwarf_siblingof(&child,&child)) {
+        MC_dwarf_handle_die(info, &child, &unit_die, NULL);
+      }
     }
     offset = next_offset;
   }

diff --git a/examples/msg/mc/bugged1_liveness_visited.tesh b/examples/msg/mc/bugged1_liveness_visited.tesh
index 7f2c2ec..2537720 100644 (file)
--- a/examples/msg/mc/bugged1_liveness_visited.tesh
+++ b/examples/msg/mc/bugged1_liveness_visited.tesh
@@ -35,8 +35,6 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de
 > [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly

-> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)

 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle


@@ -48,8 +46,6 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it

-> [  0.000000] (2:client@Boivin) Ask the request
-> [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)

 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle


@@ -61,8 +57,6 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it

-> [  0.000000] (2:client@Boivin) Ask the request
-> [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)

 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle


@@ -74,14 +68,12 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it

-> [  0.000000] (2:client@Boivin) Ask the request
-> [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)

 > [  0.000000] (3:client@Fafard) Propositions changed : r=1, cs=0
 > [  0.000000] (3:client@Fafard) Propositions changed : r=1, cs=0

-> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it

 > [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
 > [  0.000000] (2:client@Boivin) Ask the request

-> [  0.000000] (0:@) Pair 61 already reached (equal to pair 49) !
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
+> [  0.000000] (0:@) Pair 57 already reached (equal to pair 45) !

 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*


@@ -119,16 +111,16 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (54)
 > [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
 > [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (56)
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (54)
 > [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
 > [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (56)

-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)

 > [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
 > [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)

-> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)

 > [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
 > [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) (62)
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
 > [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
 > [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) (62)
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)

+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
+> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
+> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)

 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (54)
 > [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
 > [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (56)
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (54)
 > [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
 > [  0.000000] (0:@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (56)


@@ -136,11 +128,7 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
 > [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
 > [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
 > [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
 > [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)

-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) (56)
-> [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)]) (62)
-> [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
-> [  0.000000] (0:@) Expanded pairs = 61
-> [  0.000000] (0:@) Visited pairs = 224
-> [  0.000000] (0:@) Executed transitions = 223
-> [  0.000000] (0:@) Counter-example depth : 54
+> [  0.000000] (0:@) Expanded pairs = 57
+> [  0.000000] (0:@) Visited pairs = 208
+> [  0.000000] (0:@) Executed transitions = 207
+> [  0.000000] (0:@) Counter-example depth : 50

diff --git a/src/mc/mc_dwarf.c b/src/mc/mc_dwarf.c
index 5bfb6cd..69cebec 100644 (file)
--- a/src/mc/mc_dwarf.c
+++ b/src/mc/mc_dwarf.c
@@ -942,6 +942,8 @@ static void MC_dwarf_handle_children(mc_object_info_t info, Dwarf_Die* die, Dwar
 static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame) {
   int tag = dwarf_tag(die);
   switch (tag) {
 static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die* unit, dw_frame_t frame) {
   int tag = dwarf_tag(die);
   switch (tag) {

+
+    // Type:

     case DW_TAG_array_type:
     case DW_TAG_class_type:
     case DW_TAG_enumeration_type:
     case DW_TAG_array_type:
     case DW_TAG_class_type:
     case DW_TAG_enumeration_type:


@@ -966,18 +968,26 @@ static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die* die, Dwarf_Die
     case DW_TAG_shared_type:
       MC_dwarf_handle_type_die(info, die, unit);
       break;
     case DW_TAG_shared_type:
       MC_dwarf_handle_type_die(info, die, unit);
       break;

+
+    // Program:

     case DW_TAG_subprogram:
       MC_dwarf_handle_subprogram_die(info, die, unit, frame);
       return;
     case DW_TAG_subprogram:
       MC_dwarf_handle_subprogram_die(info, die, unit, frame);
       return;

-    // case DW_TAG_formal_parameter:
+
+    // Variable:

     case DW_TAG_variable:
     case DW_TAG_formal_parameter:
       MC_dwarf_handle_variable_die(info, die, unit, frame);
       break;
     case DW_TAG_variable:
     case DW_TAG_formal_parameter:
       MC_dwarf_handle_variable_die(info, die, unit, frame);
       break;

-  }

 
 

-  // Recursive processing of children DIE:
-  MC_dwarf_handle_children(info, die, unit, frame);
+    // Scope:
+    case DW_TAG_lexical_block:
+    case DW_TAG_try_block:
+    case DW_TAG_inlined_subroutine:
+      // TODO
+      break;
+
+  }

 }
 
 void MC_dwarf_get_variables(mc_object_info_t info) {
 }
 
 void MC_dwarf_get_variables(mc_object_info_t info) {


@@ -994,10 +1004,14 @@ void MC_dwarf_get_variables(mc_object_info_t info) {
   Dwarf_Off next_offset = 0;
   size_t length;
   while (dwarf_nextcu (dwarf, offset, &next_offset, &length, NULL, NULL, NULL) == 0) {
   Dwarf_Off next_offset = 0;
   size_t length;
   while (dwarf_nextcu (dwarf, offset, &next_offset, &length, NULL, NULL, NULL) == 0) {

-    Dwarf_Die die;
+    Dwarf_Die unit_die;

 
 

-    if(dwarf_offdie(dwarf, offset+length, &die)!=NULL) {
-      MC_dwarf_handle_die(info, &die, &die, NULL);
+    if(dwarf_offdie(dwarf, offset+length, &unit_die)!=NULL) {
+      Dwarf_Die child;
+      int res;
+      for (res=dwarf_child(&unit_die, &child); res==0; res=dwarf_siblingof(&child,&child)) {
+        MC_dwarf_handle_die(info, &child, &unit_die, NULL);
+      }

     }
     offset = next_offset;
   }
     }
     offset = next_offset;
   }