@@ -228,7 +228,7 @@ private class ArrayContent extends Content, TArrayContent {
228
228
private predicate fieldStoreStepNoChi ( Node node1 , FieldContent f , PostUpdateNode node2 ) {
229
229
exists ( StoreInstruction store , Class c |
230
230
store = node2 .asInstruction ( ) and
231
- store .getSourceValue ( ) = node1 .asInstruction ( ) and
231
+ store .getSourceValueOperand ( ) = node1 .asOperand ( ) and
232
232
getWrittenField ( store , f .( FieldContent ) .getAField ( ) , c ) and
233
233
f .hasOffset ( c , _, _)
234
234
)
@@ -253,27 +253,32 @@ private predicate getWrittenField(Instruction instr, Field f, Class c) {
253
253
}
254
254
255
255
private predicate fieldStoreStepChi ( Node node1 , FieldContent f , PostUpdateNode node2 ) {
256
- exists ( StoreInstruction store , ChiInstruction chi |
257
- node1 .asInstruction ( ) = store and
256
+ exists ( ChiPartialOperand operand , ChiInstruction chi |
257
+ chi .getPartialOperand ( ) = operand and
258
+ node1 .asOperand ( ) = operand and
258
259
node2 .asInstruction ( ) = chi and
259
- chi .getPartial ( ) = store and
260
260
exists ( Class c |
261
261
c = chi .getResultType ( ) and
262
262
exists ( int startBit , int endBit |
263
263
chi .getUpdatedInterval ( startBit , endBit ) and
264
264
f .hasOffset ( c , startBit , endBit )
265
265
)
266
266
or
267
- getWrittenField ( store , f .getAField ( ) , c ) and
267
+ getWrittenField ( operand . getDef ( ) , f .getAField ( ) , c ) and
268
268
f .hasOffset ( c , _, _)
269
269
)
270
270
)
271
271
}
272
272
273
273
private predicate arrayStoreStepChi ( Node node1 , ArrayContent a , PostUpdateNode node2 ) {
274
274
a = TArrayContent ( ) and
275
- exists ( StoreInstruction store |
276
- node1 .asInstruction ( ) = store and
275
+ exists ( ChiPartialOperand operand , ChiInstruction chi , StoreInstruction store |
276
+ chi .getPartialOperand ( ) = operand and
277
+ store = operand .getDef ( ) and
278
+ node1 .asOperand ( ) = operand and
279
+ // This `ChiInstruction` will always have a non-conflated result because both `ArrayStoreNode`
280
+ // and `PointerStoreNode` require it in their characteristic predicates.
281
+ node2 .asInstruction ( ) = chi and
277
282
(
278
283
// `x[i] = taint()`
279
284
// This matches the characteristic predicate in `ArrayStoreNode`.
@@ -282,10 +287,7 @@ private predicate arrayStoreStepChi(Node node1, ArrayContent a, PostUpdateNode n
282
287
// `*p = taint()`
283
288
// This matches the characteristic predicate in `PointerStoreNode`.
284
289
store .getDestinationAddress ( ) .( CopyValueInstruction ) .getUnary ( ) instanceof LoadInstruction
285
- ) and
286
- // This `ChiInstruction` will always have a non-conflated result because both `ArrayStoreNode`
287
- // and `PointerStoreNode` require it in their characteristic predicates.
288
- node2 .asInstruction ( ) .( ChiInstruction ) .getPartial ( ) = store
290
+ )
289
291
)
290
292
}
291
293
@@ -306,7 +308,7 @@ predicate storeStep(Node node1, Content f, PostUpdateNode node2) {
306
308
private predicate fieldStoreStepAfterArraySuppression (
307
309
Node node1 , FieldContent f , PostUpdateNode node2
308
310
) {
309
- exists ( BufferMayWriteSideEffectInstruction write , ChiInstruction chi , Class c |
311
+ exists ( WriteSideEffectInstruction write , ChiInstruction chi , Class c |
310
312
not chi .isResultConflated ( ) and
311
313
node1 .asInstruction ( ) = chi and
312
314
node2 .asInstruction ( ) = chi and
@@ -334,17 +336,17 @@ private predicate getLoadedField(LoadInstruction load, Field f, Class c) {
334
336
* `node2`.
335
337
*/
336
338
private predicate fieldReadStep ( Node node1 , FieldContent f , Node node2 ) {
337
- exists ( LoadInstruction load |
338
- node2 .asInstruction ( ) = load and
339
- node1 .asInstruction ( ) = load . getSourceValueOperand ( ) .getAnyDef ( ) and
339
+ exists ( LoadOperand operand |
340
+ node2 .asOperand ( ) = operand and
341
+ node1 .asInstruction ( ) = operand .getAnyDef ( ) and
340
342
exists ( Class c |
341
- c = load . getSourceValueOperand ( ) .getAnyDef ( ) .getResultType ( ) and
343
+ c = operand .getAnyDef ( ) .getResultType ( ) and
342
344
exists ( int startBit , int endBit |
343
- load . getSourceValueOperand ( ) .getUsedInterval ( unbindInt ( startBit ) , unbindInt ( endBit ) ) and
345
+ operand .getUsedInterval ( unbindInt ( startBit ) , unbindInt ( endBit ) ) and
344
346
f .hasOffset ( c , startBit , endBit )
345
347
)
346
348
or
347
- getLoadedField ( load , f .getAField ( ) , c ) and
349
+ getLoadedField ( operand . getUse ( ) , f .getAField ( ) , c ) and
348
350
f .hasOffset ( c , _, _)
349
351
)
350
352
)
@@ -365,7 +367,7 @@ private predicate fieldReadStep(Node node1, FieldContent f, Node node2) {
365
367
*/
366
368
predicate suppressArrayRead ( Node node1 , ArrayContent a , Node node2 ) {
367
369
a = TArrayContent ( ) and
368
- exists ( BufferMayWriteSideEffectInstruction write , ChiInstruction chi |
370
+ exists ( WriteSideEffectInstruction write , ChiInstruction chi |
369
371
node1 .asInstruction ( ) = write and
370
372
node2 .asInstruction ( ) = chi and
371
373
chi .getPartial ( ) = write and
@@ -386,20 +388,20 @@ private Instruction skipOneCopyValueInstructionRec(CopyValueInstruction copy) {
386
388
result = skipOneCopyValueInstructionRec ( copy .getUnary ( ) )
387
389
}
388
390
389
- private Instruction skipCopyValueInstructions ( Instruction instr ) {
390
- not result instanceof CopyValueInstruction and result = instr
391
+ private Instruction skipCopyValueInstructions ( Operand op ) {
392
+ not result instanceof CopyValueInstruction and result = op . getDef ( )
391
393
or
392
- result = skipOneCopyValueInstructionRec ( instr )
394
+ result = skipOneCopyValueInstructionRec ( op . getDef ( ) )
393
395
}
394
396
395
397
private predicate arrayReadStep ( Node node1 , ArrayContent a , Node node2 ) {
396
398
a = TArrayContent ( ) and
397
399
// Explicit dereferences such as `*p` or `p[i]` where `p` is a pointer or array.
398
- exists ( LoadInstruction load , Instruction address |
399
- load . getSourceValueOperand ( ) .isDefinitionInexact ( ) and
400
- node1 .asInstruction ( ) = load . getSourceValueOperand ( ) .getAnyDef ( ) and
401
- load = node2 .asInstruction ( ) and
402
- address = skipCopyValueInstructions ( load . getSourceAddress ( ) ) and
400
+ exists ( LoadOperand operand , Instruction address |
401
+ operand .isDefinitionInexact ( ) and
402
+ node1 .asInstruction ( ) = operand .getAnyDef ( ) and
403
+ operand = node2 .asOperand ( ) and
404
+ address = skipCopyValueInstructions ( operand . getAddressOperand ( ) ) and
403
405
(
404
406
address instanceof LoadInstruction or
405
407
address instanceof ArrayToPointerConvertInstruction or
@@ -420,18 +422,18 @@ private predicate arrayReadStep(Node node1, ArrayContent a, Node node2) {
420
422
* use(x);
421
423
* ```
422
424
* the load on `x` in `use(x)` will exactly overlap with its definition (in this case the definition
423
- * is a `BufferMayWriteSideEffect `). This predicate pops the `ArrayContent` (pushed by the store in `f`)
425
+ * is a `WriteSideEffect `). This predicate pops the `ArrayContent` (pushed by the store in `f`)
424
426
* from the access path.
425
427
*/
426
428
private predicate exactReadStep ( Node node1 , ArrayContent a , Node node2 ) {
427
429
a = TArrayContent ( ) and
428
- exists ( BufferMayWriteSideEffectInstruction write , ChiInstruction chi |
430
+ exists ( WriteSideEffectInstruction write , ChiInstruction chi |
429
431
not chi .isResultConflated ( ) and
430
432
chi .getPartial ( ) = write and
431
433
node1 .asInstruction ( ) = write and
432
434
node2 .asInstruction ( ) = chi and
433
435
// To distinquish this case from the `arrayReadStep` case we require that the entire variable was
434
- // overwritten by the `BufferMayWriteSideEffectInstruction ` (i.e., there is a load that reads the
436
+ // overwritten by the `WriteSideEffectInstruction ` (i.e., there is a load that reads the
435
437
// entire variable).
436
438
exists ( LoadInstruction load | load .getSourceValue ( ) = chi )
437
439
)
0 commit comments