@@ -24,8 +24,7 @@ module ProductFlow {
24
24
DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 , DataFlow:: PathNode sink1 ,
25
25
DataFlow2:: PathNode sink2
26
26
) {
27
- isSinkPair ( sink1 .getNode ( ) , sink2 .getNode ( ) ) and
28
- reachablePair2 ( this , source1 , source2 , sink1 , sink2 )
27
+ reachable ( this , source1 , source2 , sink1 , sink2 )
29
28
}
30
29
}
31
30
@@ -62,58 +61,59 @@ module ProductFlow {
62
61
}
63
62
}
64
63
65
- private predicate reachablePair1 (
64
+
65
+ private predicate reachableInterprocEntry (
66
66
Configuration conf , DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 ,
67
67
DataFlow:: PathNode node1 , DataFlow2:: PathNode node2
68
68
) {
69
- reachablePair ( conf , source1 , source2 , node1 , node2 )
69
+ conf .isSourcePair ( node1 .getNode ( ) , node2 .getNode ( ) ) and
70
+ node1 = source1 and
71
+ node2 = source2
70
72
or
71
- exists ( DataFlow:: PathNode mid1 |
72
- reachablePair1 ( conf , source1 , source2 , mid1 , node2 ) and
73
- mid1 .getASuccessor ( ) = node1 and
74
- mid1 .getNode ( ) .getEnclosingCallable ( ) = node1 .getNode ( ) .getEnclosingCallable ( )
73
+ exists (
74
+ DataFlow:: PathNode midEntry1 , DataFlow2:: PathNode midEntry2 , DataFlow:: PathNode midExit1 ,
75
+ DataFlow2:: PathNode midExit2
76
+ |
77
+ reachableInterprocEntry ( conf , source1 , source2 , midEntry1 , midEntry2 ) and
78
+ interprocEdgePair ( midExit1 , midExit2 , node1 , node2 ) and
79
+ localPathStep1 * ( midEntry1 , midExit1 ) and
80
+ localPathStep2 * ( midEntry2 , midExit2 )
75
81
)
76
82
}
77
83
78
- private predicate reachablePair2 (
79
- Configuration conf , DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 ,
80
- DataFlow:: PathNode node1 , DataFlow2:: PathNode node2
81
- ) {
82
- reachablePair1 ( conf , source1 , source2 , node1 , node2 ) // TODO: restrict more
83
- or
84
- exists ( DataFlow2:: PathNode mid2 |
85
- reachablePair2 ( conf , source1 , source2 , node1 , mid2 ) and
86
- mid2 .getASuccessor ( ) = node2 and
87
- mid2 .getNode ( ) .getEnclosingCallable ( ) = node2 .getNode ( ) .getEnclosingCallable ( )
88
- )
84
+ private predicate localPathStep1 ( DataFlow:: PathNode pred , DataFlow:: PathNode succ ) {
85
+ DataFlow:: PathGraph:: edges ( pred , succ ) and
86
+ pred .getNode ( ) .getEnclosingCallable ( ) = succ .getNode ( ) .getEnclosingCallable ( )
89
87
}
90
88
91
- private predicate interprocStep (
92
- Configuration conf , DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 ,
93
- DataFlow:: PathNode node1 , DataFlow2:: PathNode node2
89
+ private predicate localPathStep2 ( DataFlow2:: PathNode pred , DataFlow2:: PathNode succ ) {
90
+ DataFlow2:: PathGraph:: edges ( pred , succ ) and
91
+ pred .getNode ( ) .getEnclosingCallable ( ) = succ .getNode ( ) .getEnclosingCallable ( )
92
+ }
93
+
94
+ private predicate interprocEdgePair (
95
+ DataFlow:: PathNode pred1 , DataFlow2:: PathNode pred2 , DataFlow:: PathNode succ1 ,
96
+ DataFlow2:: PathNode succ2
94
97
) {
95
- exists ( DataFlow:: PathNode mid1 , DataFlow2:: PathNode mid2 , Function funcMid , Function func |
96
- reachablePair2 ( conf , source1 , source2 , mid1 , mid2 ) and
97
- mid1 .getASuccessor ( ) = node1 and
98
- mid2 .getASuccessor ( ) = node2 and
99
- mid1 .getNode ( ) .getEnclosingCallable ( ) = funcMid and // TODO: recursive function weirdness?
100
- mid2 .getNode ( ) .getEnclosingCallable ( ) = funcMid and
101
- node1 .getNode ( ) .getEnclosingCallable ( ) = func and
102
- node2 .getNode ( ) .getEnclosingCallable ( ) = func and
103
- funcMid != func
98
+ exists ( Declaration predDecl , Declaration succDecl |
99
+ DataFlow:: PathGraph:: edges ( pred1 , succ1 ) and
100
+ DataFlow2:: PathGraph:: edges ( pred2 , succ2 ) and
101
+ predDecl != succDecl and
102
+ pred1 .getNode ( ) .getEnclosingCallable ( ) = predDecl and
103
+ pred2 .getNode ( ) .getEnclosingCallable ( ) = predDecl and
104
+ succ1 .getNode ( ) .getEnclosingCallable ( ) = succDecl and
105
+ succ2 .getNode ( ) .getEnclosingCallable ( ) = succDecl
104
106
)
105
107
}
106
108
107
- private predicate reachablePair (
108
- Configuration conf , DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 ,
109
- DataFlow:: PathNode node1 , DataFlow2:: PathNode node2
109
+ private predicate reachable (
110
+ Configuration conf , DataFlow:: PathNode source1 , DataFlow2:: PathNode source2 , DataFlow:: PathNode sink1 , DataFlow2:: PathNode sink2
110
111
) {
111
- conf .isSourcePair ( node1 .getNode ( ) , node2 .getNode ( ) ) and
112
- node1 .isSource ( ) and
113
- node2 .isSource ( ) and
114
- source1 = node1 and
115
- source2 = node2
116
- or
117
- interprocStep ( conf , source1 , source2 , node1 , node2 )
112
+ exists ( DataFlow:: PathNode mid1 , DataFlow2:: PathNode mid2 |
113
+ reachableInterprocEntry ( conf , source1 , source2 , mid1 , mid2 ) and
114
+ conf .isSinkPair ( sink1 .getNode ( ) , sink2 .getNode ( ) ) and
115
+ localPathStep1 * ( mid1 , sink1 ) and
116
+ localPathStep2 * ( mid2 , sink2 )
117
+ )
118
118
}
119
119
}
0 commit comments