@@ -3,33 +3,42 @@ import DataFlowConfig
3
3
4
4
query predicate dataFlow ( DataFlow:: Node src , DataFlow:: Node snk ) { TestFlow:: flow ( src , snk ) }
5
5
6
- class Parity extends DataFlow:: FlowLabel {
7
- Parity ( ) { this = "even" or this = "odd" }
8
-
9
- Parity flip ( ) { result != this }
10
- }
11
-
12
6
module FlowLabelConfig implements DataFlow:: StateConfigSig {
13
- class FlowState = DataFlow:: FlowLabel ;
7
+ private newtype TFlowState =
8
+ TEven ( ) or
9
+ TOdd ( )
10
+
11
+ class FlowState extends TFlowState {
12
+ string toString ( ) {
13
+ this = TEven ( ) and result = "even"
14
+ or
15
+ this = TOdd ( ) and result = "odd"
16
+ }
17
+
18
+ FlowState flip ( ) {
19
+ this = TEven ( ) and result = TOdd ( )
20
+ or
21
+ this = TOdd ( ) and result = TEven ( )
22
+ }
23
+ }
14
24
15
- predicate isSource ( DataFlow:: Node nd , DataFlow :: FlowLabel lbl ) {
25
+ predicate isSource ( DataFlow:: Node nd , FlowState state ) {
16
26
nd .( DataFlow:: CallNode ) .getCalleeName ( ) = "source" and
17
- lbl = "even"
27
+ state = TEven ( )
18
28
}
19
29
20
- predicate isSink ( DataFlow:: Node nd , DataFlow :: FlowLabel lbl ) {
30
+ predicate isSink ( DataFlow:: Node nd , FlowState state ) {
21
31
nd = any ( DataFlow:: CallNode c | c .getCalleeName ( ) = "sink" ) .getAnArgument ( ) and
22
- lbl = "even"
32
+ state = TEven ( )
23
33
}
24
34
25
35
predicate isAdditionalFlowStep (
26
- DataFlow:: Node pred , DataFlow:: FlowLabel predLabel , DataFlow:: Node succ ,
27
- DataFlow:: FlowLabel succLabel
36
+ DataFlow:: Node node1 , FlowState state1 , DataFlow:: Node node2 , FlowState state2
28
37
) {
29
- exists ( DataFlow:: CallNode c | c = succ |
38
+ exists ( DataFlow:: CallNode c | c = node2 |
30
39
c .getCalleeName ( ) = "inc" and
31
- pred = c .getAnArgument ( ) and
32
- succLabel = predLabel . ( Parity ) .flip ( )
40
+ node1 = c .getAnArgument ( ) and
41
+ state2 = state1 .flip ( )
33
42
)
34
43
}
35
44
}
0 commit comments