@@ -234,16 +234,16 @@ signature module InputSig<LocationSig Location> {
234234 */
235235 predicate parameterMatch ( ParameterPosition ppos , ArgumentPosition apos ) ;
236236
237- /** A non-overridable method with a boolean return value . */
238- class BooleanMethod {
237+ /** A non-overridable method. */
238+ class NonOverridableMethod {
239239 Parameter getParameter ( ParameterPosition ppos ) ;
240240
241241 /** Gets an expression being returned by this method. */
242242 Expr getAReturnExpr ( ) ;
243243 }
244244
245- class BooleanMethodCall extends Expr {
246- BooleanMethod getMethod ( ) ;
245+ class NonOverridableMethodCall extends Expr {
246+ NonOverridableMethod getMethod ( ) ;
247247
248248 Expr getArgument ( ArgumentPosition apos ) ;
249249 }
@@ -998,50 +998,69 @@ module Make<LocationSig Location, InputSig<Location> Input> {
998998 final private class FinalExpr = Expr ;
999999
10001000 private class ReturnExpr extends FinalExpr {
1001- ReturnExpr ( ) { any ( BooleanMethod m ) .getAReturnExpr ( ) = this }
1001+ ReturnExpr ( ) { any ( NonOverridableMethod m ) .getAReturnExpr ( ) = this }
1002+
1003+ NonOverridableMethod getMethod ( ) { result .getAReturnExpr ( ) = this }
10021004
10031005 pragma [ nomagic]
10041006 BasicBlock getBasicBlock ( ) { result = super .getBasicBlock ( ) }
10051007 }
10061008
1007- private predicate booleanReturnGuard ( Guard guard , GuardValue val ) {
1008- guard instanceof ReturnExpr and exists ( val .asBooleanValue ( ) )
1009+ private predicate relevantCallValue ( NonOverridableMethodCall call , GuardValue val ) {
1010+ BranchImplies:: guardControls ( call , val , _, _) or
1011+ ReturnImplies:: guardControls ( call , val , _, _)
1012+ }
1013+
1014+ private predicate relevantReturnValue ( NonOverridableMethod m , GuardValue val ) {
1015+ exists ( NonOverridableMethodCall call |
1016+ relevantCallValue ( call , val ) and
1017+ call .getMethod ( ) = m and
1018+ not val instanceof TException
1019+ )
1020+ }
1021+
1022+ private predicate returnGuard ( Guard guard , GuardValue val ) {
1023+ relevantReturnValue ( guard .( ReturnExpr ) .getMethod ( ) , val )
10091024 }
10101025
1011- private module ReturnImplies = ImpliesTC< booleanReturnGuard / 2 > ;
1026+ private module ReturnImplies = ImpliesTC< returnGuard / 2 > ;
10121027
10131028 /**
10141029 * Holds if `ret` is a return expression in a non-overridable method that
10151030 * on a return value of `retval` allows the conclusion that the `ppos`th
10161031 * parameter has the value `val`.
10171032 */
10181033 private predicate validReturnInCustomGuard (
1019- ReturnExpr ret , ParameterPosition ppos , boolean retval , GuardValue val
1034+ ReturnExpr ret , ParameterPosition ppos , GuardValue retval , GuardValue val
10201035 ) {
1021- exists ( BooleanMethod m , SsaDefinition param |
1036+ exists ( NonOverridableMethod m , SsaDefinition param |
10221037 m .getAReturnExpr ( ) = ret and
10231038 parameterDefinition ( m .getParameter ( ppos ) , param )
10241039 |
10251040 exists ( Guard g0 , GuardValue v0 |
10261041 g0 .directlyValueControls ( ret .getBasicBlock ( ) , v0 ) and
10271042 BranchImplies:: ssaControls ( param , val , g0 , v0 ) and
1028- retval = [ true , false ]
1043+ relevantReturnValue ( m , retval )
10291044 )
10301045 or
1031- ReturnImplies:: ssaControls ( param , val , ret ,
1032- any ( GuardValue r | r .asBooleanValue ( ) = retval ) )
1046+ ReturnImplies:: ssaControls ( param , val , ret , retval )
10331047 )
10341048 }
10351049
10361050 /**
1037- * Gets a non-overridable method with a boolean return value that performs a check
1038- * on the `ppos`th parameter. A return value equal to `retval` allows us to conclude
1051+ * Gets a non-overridable method that performs a check on the `ppos`th
1052+ * parameter. A return value equal to `retval` allows us to conclude
10391053 * that the argument has the value `val`.
10401054 */
1041- private BooleanMethod customGuard ( ParameterPosition ppos , boolean retval , GuardValue val ) {
1055+ private NonOverridableMethod customGuard (
1056+ ParameterPosition ppos , GuardValue retval , GuardValue val
1057+ ) {
10421058 forex ( ReturnExpr ret |
10431059 result .getAReturnExpr ( ) = ret and
1044- not ret .( ConstantExpr ) .asBooleanValue ( ) = retval .booleanNot ( )
1060+ not exists ( GuardValue notRetval |
1061+ exprHasValue ( ret , notRetval ) and
1062+ disjointValues ( notRetval , retval )
1063+ )
10451064 |
10461065 validReturnInCustomGuard ( ret , ppos , retval , val )
10471066 )
@@ -1056,11 +1075,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
10561075 * custom guard wrappers.
10571076 */
10581077 predicate additionalImpliesStep ( PreGuard g1 , GuardValue v1 , PreGuard g2 , GuardValue v2 ) {
1059- exists ( BooleanMethodCall call , ParameterPosition ppos , ArgumentPosition apos |
1078+ exists ( NonOverridableMethodCall call , ParameterPosition ppos , ArgumentPosition apos |
10601079 g1 = call and
1061- call .getMethod ( ) = customGuard ( ppos , v1 . asBooleanValue ( ) , v2 ) and
1080+ call .getMethod ( ) = customGuard ( ppos , v1 , v2 ) and
10621081 call .getArgument ( apos ) = g2 and
1063- parameterMatch ( pragma [ only_bind_out ] ( ppos ) , pragma [ only_bind_out ] ( apos ) )
1082+ parameterMatch ( pragma [ only_bind_out ] ( ppos ) , pragma [ only_bind_out ] ( apos ) ) and
1083+ not exprHasValue ( g2 , v2 ) // disregard trivial guard
10641084 )
10651085 }
10661086 }
0 commit comments