@@ -736,6 +736,15 @@ predicate addressFlowInstrRTC(Instruction iFrom, Instruction iTo) {
736736 AddressFlow:: addressFlowInstrTC ( iFrom , iTo )
737737}
738738
739+ /**
740+ * Holds if `iFrom` is the initial address of an address computation and the value computed
741+ * by `iFrom` flows to `iTo`.
742+ */
743+ private predicate initialAddressFlowInstrRTC ( Instruction iFrom , Instruction iTo ) {
744+ isInitialAddress ( iFrom ) and
745+ addressFlowInstrRTC ( iFrom , iTo )
746+ }
747+
739748/**
740749 * Holds if `instr2` is a possible (transitive) successor of `instr1` in the control-flow graph.
741750 *
@@ -753,17 +762,53 @@ private predicate isSuccessorInstruction(Instruction instr1, Instruction instr2)
753762 block2 .getInstruction ( index2 ) = instr2 and
754763 index1 < index2
755764 )
756- else block1 . getASuccessor + ( ) = block2
765+ else IRBlockFlow :: flowsToSink ( block1 , block2 )
757766 )
758767}
759768
760769/**
761- * Holds if `iFrom` is the initial address of an address computation and the value computed
762- * by `iFrom` flows to `iTo `.
770+ * A module that hides implementation details for the control-flow analysis needed
771+ * for `isSuccessorInstruction `.
763772 */
764- private predicate initialAddressFlowInstrRTC ( Instruction iFrom , Instruction iTo ) {
765- isInitialAddress ( iFrom ) and
766- addressFlowInstrRTC ( iFrom , iTo )
773+ private module IRBlockFlow {
774+ /**
775+ * Holds if:
776+ * - `source` and `sink` are either a `LoadInstruction` or a `ReadSideEffectInstruction`.
777+ * - `source` is the beginning of an address computation that is used as part of a `storeStep`,
778+ * and `sink` is the beginning of an address computation that is used as part of a `readStep`.
779+ * - `source` and `sink` read from the same instruction (i.e., the definition of their memory operand
780+ * is identical).
781+ */
782+ private predicate sourceSinkPairCand ( Instruction source , Instruction sink ) {
783+ source != sink and
784+ initialAddressFlowInstrRTC ( any ( AddressNodeStore address ) .getInstruction ( ) ,
785+ getSourceAddress ( source ) ) and
786+ getSourceValue ( source ) = getSourceValue ( sink ) and
787+ initialAddressFlowInstrRTC ( any ( AddressNodeRead address ) .getInstruction ( ) , getSourceAddress ( sink ) )
788+ }
789+
790+ private predicate isSource ( IRBlock source ) { sourceSinkPairCand ( source .getAnInstruction ( ) , _) }
791+
792+ private predicate isSink ( IRBlock sink ) { sourceSinkPairCand ( _, sink .getAnInstruction ( ) ) }
793+
794+ private IRBlock getASuccessor ( IRBlock b ) { b .getASuccessor ( ) = result }
795+
796+ private IRBlock getAPredecessor ( IRBlock b ) { b = getASuccessor ( result ) }
797+
798+ private predicate flowsFromSource ( IRBlock b ) {
799+ isSource ( b ) or
800+ flowsFromSource ( getAPredecessor ( b ) )
801+ }
802+
803+ /** Holds if `isSink(sink)` and `b` flows to `sink` in one or more steps. */
804+ predicate flowsToSink ( IRBlock b , IRBlock sink ) {
805+ flowsFromSource ( b ) and
806+ (
807+ getASuccessor ( b ) = sink and isSink ( b )
808+ or
809+ flowsToSink ( getASuccessor ( b ) , sink )
810+ )
811+ }
767812}
768813
769814/**
0 commit comments