forked from system-pclub/GCatch
/
z3Node.go
129 lines (121 loc) · 2.89 KB
/
z3Node.go
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
package syncgraph
func (s *ZNodeNbSend) hasPairWith(r *ZNodeNbRecv) bool {
for _, pair := range s.Pairs {
if pair.Recv == r {
return true
}
}
return false
}
func (s *ZNodeNbSend) findOtherThreadRecvs() (result []*ZNodeNbRecv) {
for _, zthread := range s.ZGoroutine.Z3Sys.vecZGoroutines {
if zthread == s.ZGoroutine {
continue
}
for _, znode := range zthread.Nodes {
zrecv, ok := znode.(*ZNodeNbRecv)
if !ok {
continue
}
if zrecv.boolIsBlocking {
continue
}
if zrecv.PtrPNode.Node.(SyncOp).MapSyncOp()[s.PtrPNode.Node.(SyncOp)] {
result = append(result, zrecv)
}
}
}
return
}
func (r *ZNodeNbRecv) hasPairWith(s *ZNodeNbSend) bool {
for _, pair := range r.Pairs {
if pair.Send == s {
return true
}
}
return false
}
func (r *ZNodeNbRecv) findOtherThreadSends() (result []*ZNodeNbSend) {
for _, zthread := range r.ZGoroutine.Z3Sys.vecZGoroutines {
if zthread == r.ZGoroutine {
continue
}
for _, znode := range zthread.Nodes {
zsend, ok := znode.(*ZNodeNbSend)
if !ok {
continue
}
if zsend.boolIsBlocking {
continue
}
if zsend.PtrPNode.Node.(SyncOp).MapSyncOp()[r.PtrPNode.Node.(SyncOp)] {
result = append(result, zsend)
}
}
}
return
}
func (r *ZNodeNbRecv) findAllThreadCloses() (result []*ZNodeClose) {
for _, zthread := range r.ZGoroutine.Z3Sys.vecZGoroutines {
for _, znode := range zthread.Nodes {
zclose, ok := znode.(*ZNodeClose)
if !ok {
continue
}
if zclose.PtrPNode.Node.(SyncOp).MapSyncOp()[r.PtrPNode.Node.(SyncOp)] {
result = append(result, zclose)
}
}
}
return
}
func (s *ZNodeBSend) findAllThreadOtherSendRecv() (result []ZNode) {
for _, zthread := range s.ZGoroutine.Z3Sys.vecZGoroutines {
for _, znode := range zthread.Nodes {
if znode == s {
continue
}
_, is_B_send := znode.(*ZNodeBSend)
_, is_B_recv := znode.(*ZNodeBRecv)
if is_B_send == false && is_B_recv == false {
continue
}
if s.PtrPNode.Node.(SyncOp).MapSyncOp()[znode.PNode().Node.(SyncOp)] {
result = append(result, znode)
}
}
}
return
}
func (r *ZNodeBRecv) findAllThreadOtherSendRecv() (result []ZNode) {
for _, zthread := range r.ZGoroutine.Z3Sys.vecZGoroutines {
for _, znode := range zthread.Nodes {
if znode == r {
continue
}
_, is_B_send := znode.(*ZNodeBSend)
_, is_B_recv := znode.(*ZNodeBRecv)
if is_B_send == false && is_B_recv == false {
continue
}
if r.PtrPNode.Node.(SyncOp).MapSyncOp()[znode.PNode().Node.(SyncOp)] {
result = append(result, znode)
}
}
}
return
}
func (r *ZNodeBRecv) findAllThreadCloses() (result []*ZNodeClose) {
for _, zthread := range r.ZGoroutine.Z3Sys.vecZGoroutines {
for _, znode := range zthread.Nodes {
zclose, ok := znode.(*ZNodeClose)
if !ok {
continue
}
if zclose.PtrPNode.Node.(SyncOp).MapSyncOp()[r.PtrPNode.Node.(SyncOp)] {
result = append(result, zclose)
}
}
}
return
}