@@ -113,43 +113,59 @@ predicate checksPath(Expr check, Expr checkPath) {
113113 )
114114}
115115
116+ pragma [ nomagic]
117+ predicate checkPathControlsUse ( Expr check , Expr checkPath , Expr use ) {
118+ exists ( GuardCondition guard | referenceTo ( check , guard .getAChild * ( ) ) |
119+ guard .controls ( use .getBasicBlock ( ) , _)
120+ ) and
121+ checksPath ( pragma [ only_bind_into ] ( check ) , checkPath )
122+ }
123+
124+ pragma [ nomagic]
125+ predicate fileNameOperationControlsUse ( Expr check , Expr checkPath , Expr use ) {
126+ exists ( GuardCondition guard | referenceTo ( check , guard .getAChild * ( ) ) |
127+ guard .controls ( use .getBasicBlock ( ) , _)
128+ ) and
129+ pragma [ only_bind_into ] ( check ) = filenameOperation ( checkPath )
130+ }
131+
116132predicate checkUse ( Expr check , Expr checkPath , FunctionCall use , Expr usePath ) {
133+ // `check` is part of a guard that controls `use`
134+ checkPathControlsUse ( check , checkPath , use ) and
117135 // `check` looks like a check on a filename
118136 checksPath ( check , checkPath ) and
119137 // `op` looks like an operation on a filename
120138 use = filenameOperation ( usePath )
121139 or
140+ // `check` is part of a guard that controls `use`
141+ fileNameOperationControlsUse ( check , checkPath , use ) and
122142 // another filename operation (null pointers can indicate errors)
123143 check = filenameOperation ( checkPath ) and
124144 // `op` looks like a sensitive operation on a filename
125145 use = sensitiveFilenameOperation ( usePath )
126146}
127147
128148pragma [ noinline]
129- Expr getACheckedPath ( Expr check , SsaDefinition def , StackVariable v ) {
130- checkUse ( check , result , _, _) and
131- def .getAUse ( v ) = result
149+ predicate isCheckedPath (
150+ Expr check , SsaDefinition def , StackVariable v , FunctionCall use , Expr usePath , Expr checkPath
151+ ) {
152+ checkUse ( check , checkPath , use , usePath ) and
153+ def .getAUse ( v ) = checkPath
132154}
133155
134156pragma [ noinline]
135- Expr getAUsedPath ( FunctionCall use , SsaDefinition def , StackVariable v ) {
136- checkUse ( _, _, use , result ) and
137- def .getAUse ( v ) = result
157+ predicate isUsedPath (
158+ Expr check , SsaDefinition def , StackVariable v , FunctionCall use , Expr usePath , Expr checkPath
159+ ) {
160+ checkUse ( check , checkPath , use , usePath ) and
161+ def .getAUse ( v ) = usePath
138162}
139163
140- from Expr check , Expr checkPath , FunctionCall use , Expr usePath
164+ from Expr check , Expr checkPath , FunctionCall use , Expr usePath , SsaDefinition def , StackVariable v
141165where
142- checkUse ( check , checkPath , use , usePath ) and
143166 // `checkPath` and `usePath` refer to the same SSA variable
144- exists ( SsaDefinition def , StackVariable v |
145- getACheckedPath ( check , def , v ) = checkPath and
146- getAUsedPath ( use , def , v ) = usePath
147- ) and
148- // the return value of `check` is used (possibly with one step of
149- // variable indirection) in a guard which controls `use`
150- exists ( GuardCondition guard | referenceTo ( check , guard .getAChild * ( ) ) |
151- guard .controls ( use .getBasicBlock ( ) , _)
152- )
167+ isCheckedPath ( check , def , v , use , usePath , checkPath ) and
168+ isUsedPath ( check , def , v , use , usePath , checkPath )
153169select use ,
154170 "The $@ being operated upon was previously $@, but the underlying file may have been changed since then." ,
155171 usePath , "filename" , check , "checked"
0 commit comments