@@ -184,7 +184,8 @@ private class FieldContent extends Content, TFieldContent {
184184
185185 FieldContent ( ) { this = TFieldContent ( c , startBit , endBit ) }
186186
187- override string toString ( ) { result = getField ( ) .toString ( ) }
187+ // Ensure that there's just 1 result for `toString`.
188+ override string toString ( ) { result = min ( Field f | f = getField ( ) | f .toString ( ) ) }
188189
189190 predicate hasOffset ( Class cl , int start , int end ) { cl = c and start = startBit and end = endBit }
190191
@@ -200,10 +201,20 @@ private class ArrayContent extends Content, TArrayContent {
200201}
201202
202203private predicate storeStepNoChi ( Node node1 , Content f , PostUpdateNode node2 ) {
203- exists ( StoreInstruction store |
204+ exists ( StoreInstruction store , Class c |
204205 store = node2 .asInstruction ( ) and
205206 store .getSourceValue ( ) = node1 .asInstruction ( ) and
206- f .( FieldContent ) .getField ( ) = store .getDestinationAddress ( ) .( FieldInstruction ) .getField ( )
207+ getWrittenField ( store , f .( FieldContent ) .getField ( ) , c ) and
208+ f .( FieldContent ) .hasOffset ( c , _, _)
209+ )
210+ }
211+
212+ pragma [ noinline]
213+ private predicate getWrittenField ( StoreInstruction store , Field f , Class c ) {
214+ exists ( FieldAddressInstruction fa |
215+ fa = store .getDestinationAddress ( ) and
216+ f = fa .getField ( ) and
217+ c = f .getDeclaringType ( )
207218 )
208219}
209220
@@ -212,13 +223,15 @@ private predicate storeStepChi(Node node1, Content f, PostUpdateNode node2) {
212223 node1 .asInstruction ( ) = store and
213224 node2 .asInstruction ( ) = chi and
214225 chi .getPartial ( ) = store and
215- (
226+ exists ( Class c |
227+ c = chi .getResultType ( ) and
216228 exists ( int startBit , int endBit |
217229 chi .getUpdatedInterval ( startBit , endBit ) and
218- f .( FieldContent ) .hasOffset ( chi . getResultType ( ) , startBit , endBit )
230+ f .( FieldContent ) .hasOffset ( c , startBit , endBit )
219231 )
220232 or
221- f .( FieldContent ) .getField ( ) = store .getDestinationAddress ( ) .( FieldInstruction ) .getField ( )
233+ getWrittenField ( store , f .( FieldContent ) .getField ( ) , c ) and
234+ f .( FieldContent ) .hasOffset ( c , _, _)
222235 )
223236 )
224237}
@@ -236,6 +249,15 @@ predicate storeStep(Node node1, Content f, PostUpdateNode node2) {
236249bindingset [ result , i]
237250private int unbindInt ( int i ) { i <= result and i >= result }
238251
252+ pragma [ noinline]
253+ private predicate getLoadedField ( LoadInstruction load , Field f , Class c ) {
254+ exists ( FieldAddressInstruction fa |
255+ fa = load .getSourceAddress ( ) and
256+ f = fa .getField ( ) and
257+ c = f .getDeclaringType ( )
258+ )
259+ }
260+
239261/**
240262 * Holds if data can flow from `node1` to `node2` via a read of `f`.
241263 * Thus, `node1` references an object with a field `f` whose value ends up in
@@ -245,14 +267,15 @@ predicate readStep(Node node1, Content f, Node node2) {
245267 exists ( LoadInstruction load |
246268 node2 .asInstruction ( ) = load and
247269 node1 .asInstruction ( ) = load .getSourceValueOperand ( ) .getAnyDef ( ) and
248- (
249- exists ( Class c , int startBit , int endBit |
250- c = load . getSourceValueOperand ( ) . getAnyDef ( ) . getResultType ( ) and
270+ exists ( Class c |
271+ c = load . getSourceValueOperand ( ) . getAnyDef ( ) . getResultType ( ) and
272+ exists ( int startBit , int endBit |
251273 load .getSourceValueOperand ( ) .getUsedInterval ( unbindInt ( startBit ) , unbindInt ( endBit ) ) and
252274 f .( FieldContent ) .hasOffset ( c , startBit , endBit )
253275 )
254276 or
255- f .( FieldContent ) .getField ( ) = load .getSourceAddress ( ) .( FieldInstruction ) .getField ( )
277+ getLoadedField ( load , f .( FieldContent ) .getField ( ) , c ) and
278+ f .( FieldContent ) .hasOffset ( c , _, _)
256279 )
257280 )
258281}
0 commit comments