@@ -70,6 +70,31 @@ predicate destroyedToBeginSink(DataFlow::Node sink, FunctionCall fc) {
70
70
)
71
71
}
72
72
73
+ /**
74
+ * Holds if `node1` is the node corresponding to a qualifier of a destructor
75
+ * call and `node2` is a node that is destroyed as a result of `node1` being
76
+ * destroyed.
77
+ */
78
+ private predicate qualifierToDestroyed ( DataFlow:: Node node1 , DataFlow:: Node node2 ) {
79
+ tempToDestructorSink ( node1 , _) and
80
+ node2 = getADestroyedNode ( node1 )
81
+ }
82
+
83
+ /**
84
+ * A configuration to track flow from a destroyed node to a qualifier of
85
+ * a `begin` or `end` function call.
86
+ *
87
+ * This configuration exists to prevent a cartesian product between all sinks and
88
+ * all states in `Config::isSink`.
89
+ */
90
+ module Config0 implements DataFlow:: ConfigSig {
91
+ predicate isSource ( DataFlow:: Node source ) { qualifierToDestroyed ( _, source ) }
92
+
93
+ predicate isSink ( DataFlow:: Node sink ) { destroyedToBeginSink ( sink , _) }
94
+ }
95
+
96
+ module Flow0 = DataFlow:: Global< Config0 > ;
97
+
73
98
/**
74
99
* A configuration to track flow from a temporary variable to the qualifier of
75
100
* a destructor call, and subsequently to a qualifier of a call to `begin` or
@@ -79,12 +104,15 @@ module Config implements DataFlow::StateConfigSig {
79
104
newtype FlowState =
80
105
additional TempToDestructor ( ) or
81
106
additional DestroyedToBegin ( DataFlow:: Node n ) {
82
- exists ( DataFlow:: Node thisOperand |
83
- tempToDestructorSink ( thisOperand , _) and
84
- n = getADestroyedNode ( thisOperand )
85
- )
107
+ any ( Flow0:: PathNode pn | pn .isSource ( ) ) .getNode ( ) = n
86
108
}
87
109
110
+ /**
111
+ * Holds if `sink` is a qualifier to a call to `begin`, and `mid` is an
112
+ * object that is destroyed.
113
+ */
114
+ private predicate relevant ( DataFlow:: Node mid , DataFlow:: Node sink ) { Flow0:: flow ( mid , sink ) }
115
+
88
116
predicate isSource ( DataFlow:: Node source , FlowState state ) {
89
117
source .asInstruction ( ) .( VariableAddressInstruction ) .getIRVariable ( ) instanceof IRTempVariable and
90
118
state = TempToDestructor ( )
@@ -93,16 +121,16 @@ module Config implements DataFlow::StateConfigSig {
93
121
predicate isAdditionalFlowStep (
94
122
DataFlow:: Node node1 , FlowState state1 , DataFlow:: Node node2 , FlowState state2
95
123
) {
96
- tempToDestructorSink ( node1 , _) and
97
124
state1 = TempToDestructor ( ) and
98
125
state2 = DestroyedToBegin ( node2 ) and
99
- node2 = getADestroyedNode ( node1 )
126
+ qualifierToDestroyed ( node1 , node2 )
100
127
}
101
128
102
129
predicate isSink ( DataFlow:: Node sink , FlowState state ) {
103
- // Note: This is a non-trivial cartesian product!
104
- // Hopefully, both of these sets are quite small in practice
105
- destroyedToBeginSink ( sink , _) and state instanceof DestroyedToBegin
130
+ exists ( DataFlow:: Node mid |
131
+ relevant ( mid , sink ) and
132
+ state = DestroyedToBegin ( mid )
133
+ )
106
134
}
107
135
108
136
DataFlow:: FlowFeature getAFeature ( ) {
0 commit comments