@@ -228,7 +228,7 @@ private class ArrayContent extends Content, TArrayContent {
228228private predicate fieldStoreStepNoChi ( Node node1 , FieldContent f , PostUpdateNode node2 ) {
229229 exists ( StoreInstruction store , Class c |
230230 store = node2 .asInstruction ( ) and
231- store .getSourceValue ( ) = node1 .asInstruction ( ) and
231+ store .getSourceValueOperand ( ) = node1 .asOperand ( ) and
232232 getWrittenField ( store , f .( FieldContent ) .getAField ( ) , c ) and
233233 f .hasOffset ( c , _, _)
234234 )
@@ -253,27 +253,32 @@ private predicate getWrittenField(Instruction instr, Field f, Class c) {
253253}
254254
255255private 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
258259 node2 .asInstruction ( ) = chi and
259- chi .getPartial ( ) = store and
260260 exists ( Class c |
261261 c = chi .getResultType ( ) and
262262 exists ( int startBit , int endBit |
263263 chi .getUpdatedInterval ( startBit , endBit ) and
264264 f .hasOffset ( c , startBit , endBit )
265265 )
266266 or
267- getWrittenField ( store , f .getAField ( ) , c ) and
267+ getWrittenField ( operand . getDef ( ) , f .getAField ( ) , c ) and
268268 f .hasOffset ( c , _, _)
269269 )
270270 )
271271}
272272
273273private predicate arrayStoreStepChi ( Node node1 , ArrayContent a , PostUpdateNode node2 ) {
274274 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
277282 (
278283 // `x[i] = taint()`
279284 // This matches the characteristic predicate in `ArrayStoreNode`.
@@ -282,10 +287,7 @@ private predicate arrayStoreStepChi(Node node1, ArrayContent a, PostUpdateNode n
282287 // `*p = taint()`
283288 // This matches the characteristic predicate in `PointerStoreNode`.
284289 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+ )
289291 )
290292}
291293
@@ -306,7 +308,7 @@ predicate storeStep(Node node1, Content f, PostUpdateNode node2) {
306308private predicate fieldStoreStepAfterArraySuppression (
307309 Node node1 , FieldContent f , PostUpdateNode node2
308310) {
309- exists ( BufferMayWriteSideEffectInstruction write , ChiInstruction chi , Class c |
311+ exists ( WriteSideEffectInstruction write , ChiInstruction chi , Class c |
310312 not chi .isResultConflated ( ) and
311313 node1 .asInstruction ( ) = chi and
312314 node2 .asInstruction ( ) = chi and
@@ -334,17 +336,17 @@ private predicate getLoadedField(LoadInstruction load, Field f, Class c) {
334336 * `node2`.
335337 */
336338private 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
340342 exists ( Class c |
341- c = load . getSourceValueOperand ( ) .getAnyDef ( ) .getResultType ( ) and
343+ c = operand .getAnyDef ( ) .getResultType ( ) and
342344 exists ( int startBit , int endBit |
343- load . getSourceValueOperand ( ) .getUsedInterval ( unbindInt ( startBit ) , unbindInt ( endBit ) ) and
345+ operand .getUsedInterval ( unbindInt ( startBit ) , unbindInt ( endBit ) ) and
344346 f .hasOffset ( c , startBit , endBit )
345347 )
346348 or
347- getLoadedField ( load , f .getAField ( ) , c ) and
349+ getLoadedField ( operand . getUse ( ) , f .getAField ( ) , c ) and
348350 f .hasOffset ( c , _, _)
349351 )
350352 )
@@ -365,7 +367,7 @@ private predicate fieldReadStep(Node node1, FieldContent f, Node node2) {
365367 */
366368predicate suppressArrayRead ( Node node1 , ArrayContent a , Node node2 ) {
367369 a = TArrayContent ( ) and
368- exists ( BufferMayWriteSideEffectInstruction write , ChiInstruction chi |
370+ exists ( WriteSideEffectInstruction write , ChiInstruction chi |
369371 node1 .asInstruction ( ) = write and
370372 node2 .asInstruction ( ) = chi and
371373 chi .getPartial ( ) = write and
@@ -386,20 +388,20 @@ private Instruction skipOneCopyValueInstructionRec(CopyValueInstruction copy) {
386388 result = skipOneCopyValueInstructionRec ( copy .getUnary ( ) )
387389}
388390
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 ( )
391393 or
392- result = skipOneCopyValueInstructionRec ( instr )
394+ result = skipOneCopyValueInstructionRec ( op . getDef ( ) )
393395}
394396
395397private predicate arrayReadStep ( Node node1 , ArrayContent a , Node node2 ) {
396398 a = TArrayContent ( ) and
397399 // 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
403405 (
404406 address instanceof LoadInstruction or
405407 address instanceof ArrayToPointerConvertInstruction or
@@ -420,18 +422,18 @@ private predicate arrayReadStep(Node node1, ArrayContent a, Node node2) {
420422 * use(x);
421423 * ```
422424 * 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`)
424426 * from the access path.
425427 */
426428private predicate exactReadStep ( Node node1 , ArrayContent a , Node node2 ) {
427429 a = TArrayContent ( ) and
428- exists ( BufferMayWriteSideEffectInstruction write , ChiInstruction chi |
430+ exists ( WriteSideEffectInstruction write , ChiInstruction chi |
429431 not chi .isResultConflated ( ) and
430432 chi .getPartial ( ) = write and
431433 node1 .asInstruction ( ) = write and
432434 node2 .asInstruction ( ) = chi and
433435 // 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
435437 // entire variable).
436438 exists ( LoadInstruction load | load .getSourceValue ( ) = chi )
437439 )
0 commit comments