@@ -65,23 +65,21 @@ class ScanfOutput extends Expr {
65
65
* but before it gets reset or reused in another `scanf` call.
66
66
*/
67
67
Access getAnAccess ( ) {
68
- exists ( Instruction dst |
69
- this .bigStep ( ) = dst and
70
- dst .getAst ( ) = result and
71
- valueNumber ( dst ) = valNum
68
+ exists ( Instruction source , Instruction sink |
69
+ this .hasFlow ( source , sink ) and
70
+ sink .getAst ( ) = result
72
71
)
73
72
}
74
73
75
- private Instruction bigStep ( ) {
76
- result = this . smallStep ( instr )
77
- or
78
- exists ( Instruction i | i = this . bigStep ( ) | result = this . smallStep ( i ) )
79
- }
74
+ // --- definition of the flow graph ---
75
+ pragma [ inline ]
76
+ private predicate isEdge ( Instruction i , Instruction j ) { i . getASuccessor ( ) = j }
77
+
78
+ private predicate isSource ( Instruction i ) { i = instr }
80
79
81
- private Instruction smallStep ( Instruction i ) {
82
- instr .getASuccessor * ( ) = i and
83
- i .getASuccessor ( ) = result and
84
- not this .isBarrier ( result )
80
+ private predicate isSink ( Instruction i ) {
81
+ valueNumber ( i ) = valNum and
82
+ i .getAst ( ) instanceof Access
85
83
}
86
84
87
85
private predicate isBarrier ( Instruction i ) {
@@ -92,6 +90,42 @@ class ScanfOutput extends Expr {
92
90
[ e , e .getParent ( ) .( AddressOfExpr ) ] instanceof ScanfOutput
93
91
)
94
92
}
93
+
94
+ // --- flow graph search implementation ---
95
+ private predicate hasFlow ( Instruction source , Instruction sink ) {
96
+ this .isSource ( source ) and
97
+ this .isSink ( sink ) and
98
+ this .multiStep ( source , sink )
99
+ }
100
+
101
+ private predicate multiStep ( Instruction i , Instruction j ) {
102
+ this .prunedStep ( i , j )
103
+ or
104
+ exists ( Instruction ij | this .multiStep ( i , ij ) | this .prunedStep ( ij , j ) )
105
+ }
106
+
107
+ private predicate prunedStep ( Instruction i , Instruction j ) {
108
+ this .reachedFromSource ( i ) and
109
+ this .reachesSink ( j ) and
110
+ this .oneStep ( i , j )
111
+ }
112
+
113
+ pragma [ inline]
114
+ private predicate oneStep ( Instruction i , Instruction j ) {
115
+ this .isEdge ( i , j ) and not this .isBarrier ( j )
116
+ }
117
+
118
+ private predicate reachedFromSource ( Instruction i ) {
119
+ isSource ( i )
120
+ or
121
+ exists ( Instruction h | reachedFromSource ( h ) | oneStep ( h , i ) )
122
+ }
123
+
124
+ private predicate reachesSink ( Instruction i ) {
125
+ isSink ( i )
126
+ or
127
+ exists ( Instruction j | reachesSink ( j ) | oneStep ( i , j ) )
128
+ }
95
129
}
96
130
97
131
/** Returns a block guarded by the assertion of `value op call` */
0 commit comments