@@ -101,35 +101,43 @@ module ParameterSinks {
101
101
)
102
102
}
103
103
104
- private CallInstruction getAnAlwaysReachedCallInstruction ( IRFunction f ) {
105
- result .getBlock ( ) .postDominates ( f .getEntryBlock ( ) )
104
+ private CallInstruction getAnAlwaysReachedCallInstruction ( ) {
105
+ exists ( IRFunction f | result .getBlock ( ) .postDominates ( f .getEntryBlock ( ) ) )
106
106
}
107
107
108
108
pragma [ nomagic]
109
- predicate callHasTargetAndArgument ( Function f , int i , CallInstruction call , Instruction argument ) {
110
- call .getStaticCallTarget ( ) = f and
111
- call .getArgument ( i ) = argument
109
+ private predicate callHasTargetAndArgument ( Function f , int i , Instruction argument ) {
110
+ exists ( CallInstruction call |
111
+ call .getStaticCallTarget ( ) = f and
112
+ call .getArgument ( i ) = argument and
113
+ call = getAnAlwaysReachedCallInstruction ( )
114
+ )
115
+ }
116
+
117
+ pragma [ nomagic]
118
+ private predicate initializeParameterInFunction ( Function f , int i ) {
119
+ exists ( InitializeParameterInstruction init |
120
+ pragma [ only_bind_out ] ( init .getEnclosingFunction ( ) ) = f and
121
+ init .hasIndex ( i ) and
122
+ init = getAnAlwaysDereferencedParameter ( )
123
+ )
112
124
}
113
125
114
126
pragma [ nomagic]
115
- predicate initializeParameterInFunction ( Function f , int i , InitializeParameterInstruction init ) {
116
- pragma [ only_bind_out ] ( init .getEnclosingFunction ( ) ) = f and
117
- init .hasIndex ( i )
127
+ private predicate alwaysDereferencedArgumentHasValueNumber ( ValueNumber vn ) {
128
+ exists ( int i , Function f , Instruction argument |
129
+ callHasTargetAndArgument ( f , i , argument ) and
130
+ initializeParameterInFunction ( pragma [ only_bind_into ] ( f ) , pragma [ only_bind_into ] ( i ) ) and
131
+ vn .getAnInstruction ( ) = argument
132
+ )
118
133
}
119
134
120
135
InitializeParameterInstruction getAnAlwaysDereferencedParameter ( ) {
121
136
result = getAnAlwaysDereferencedParameter0 ( )
122
137
or
123
- exists (
124
- CallInstruction call , int i , InitializeParameterInstruction p , Instruction argument ,
125
- Function f
126
- |
127
- callHasTargetAndArgument ( f , i , call , argument ) and
128
- initializeParameterInFunction ( f , i , p ) and
129
- p = getAnAlwaysDereferencedParameter ( ) and
130
- result =
131
- pragma [ only_bind_out ] ( pragma [ only_bind_into ] ( valueNumber ( argument ) ) .getAnInstruction ( ) ) and
132
- call = getAnAlwaysReachedCallInstruction ( _)
138
+ exists ( ValueNumber vn |
139
+ alwaysDereferencedArgumentHasValueNumber ( vn ) and
140
+ vn .getAnInstruction ( ) = result
133
141
)
134
142
}
135
143
}
0 commit comments