@@ -18,7 +18,7 @@ import semmle.code.cpp.commons.Scanf
1818import semmle.code.cpp.controlflow.Guards
1919import semmle.code.cpp.dataflow.new.DataFlow:: DataFlow
2020import semmle.code.cpp.ir.IR
21- import semmle.code.cpp.ir.ValueNumbering
21+ import semmle.code.cpp.valuenumbering.GlobalValueNumbering
2222import ScanfChecks
2323import ScanfToUseFlow:: PathGraph
2424
@@ -155,31 +155,20 @@ predicate hasNonGuardedAccess(
155155 flowPath ( source , call , index , sink , e ) and
156156 minGuard = getMinimumGuardConstant ( call , index )
157157 |
158- not exists ( int value |
159- e .getBasicBlock ( ) = blockGuardedBy ( value , "==" , call ) and minGuard <= value
158+ not exists ( GuardCondition guard |
159+ // call == k and k >= minGuard so call >= minGuard
160+ guard
161+ .ensuresEq ( globalValueNumber ( call ) .getAnExpr ( ) , any ( int k | minGuard <= k ) ,
162+ e .getBasicBlock ( ) , true )
160163 or
161- e .getBasicBlock ( ) = blockGuardedBy ( value , "<" , call ) and minGuard - 1 <= value
162- or
163- e .getBasicBlock ( ) = blockGuardedBy ( value , "<=" , call ) and minGuard <= value
164+ // call >= k and k >= minGuard so call >= minGuard
165+ guard
166+ .ensuresLt ( globalValueNumber ( call ) .getAnExpr ( ) , any ( int k | minGuard <= k ) ,
167+ e .getBasicBlock ( ) , false )
164168 )
165169 )
166170}
167171
168- /** Returns a block guarded by the assertion of `value op call` */
169- BasicBlock blockGuardedBy ( int value , string op , ScanfFunctionCall call ) {
170- exists ( GuardCondition g , Expr left , Expr right |
171- right = g .getAChild ( ) and
172- value = left .getValue ( ) .toInt ( ) and
173- localExprFlow ( call , right )
174- |
175- g .ensuresEq ( left , right , 0 , result , true ) and op = "=="
176- or
177- g .ensuresLt ( left , right , 0 , result , true ) and op = "<"
178- or
179- g .ensuresLt ( left , right , 1 , result , true ) and op = "<="
180- )
181- }
182-
183172from
184173 ScanfToUseFlow:: PathNode source , ScanfToUseFlow:: PathNode sink , ScanfFunctionCall call , Expr e ,
185174 int minGuard
0 commit comments