@@ -234,16 +234,16 @@ signature module InputSig<LocationSig Location> {
234
234
*/
235
235
predicate parameterMatch ( ParameterPosition ppos , ArgumentPosition apos ) ;
236
236
237
- /** A non-overridable method with a boolean return value . */
238
- class BooleanMethod {
237
+ /** A non-overridable method. */
238
+ class NonOverridableMethod {
239
239
Parameter getParameter ( ParameterPosition ppos ) ;
240
240
241
241
/** Gets an expression being returned by this method. */
242
242
Expr getAReturnExpr ( ) ;
243
243
}
244
244
245
- class BooleanMethodCall extends Expr {
246
- BooleanMethod getMethod ( ) ;
245
+ class NonOverridableMethodCall extends Expr {
246
+ NonOverridableMethod getMethod ( ) ;
247
247
248
248
Expr getArgument ( ArgumentPosition apos ) ;
249
249
}
@@ -998,50 +998,69 @@ module Make<LocationSig Location, InputSig<Location> Input> {
998
998
final private class FinalExpr = Expr ;
999
999
1000
1000
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 }
1002
1004
1003
1005
pragma [ nomagic]
1004
1006
BasicBlock getBasicBlock ( ) { result = super .getBasicBlock ( ) }
1005
1007
}
1006
1008
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 )
1009
1024
}
1010
1025
1011
- private module ReturnImplies = ImpliesTC< booleanReturnGuard / 2 > ;
1026
+ private module ReturnImplies = ImpliesTC< returnGuard / 2 > ;
1012
1027
1013
1028
/**
1014
1029
* Holds if `ret` is a return expression in a non-overridable method that
1015
1030
* on a return value of `retval` allows the conclusion that the `ppos`th
1016
1031
* parameter has the value `val`.
1017
1032
*/
1018
1033
private predicate validReturnInCustomGuard (
1019
- ReturnExpr ret , ParameterPosition ppos , boolean retval , GuardValue val
1034
+ ReturnExpr ret , ParameterPosition ppos , GuardValue retval , GuardValue val
1020
1035
) {
1021
- exists ( BooleanMethod m , SsaDefinition param |
1036
+ exists ( NonOverridableMethod m , SsaDefinition param |
1022
1037
m .getAReturnExpr ( ) = ret and
1023
1038
parameterDefinition ( m .getParameter ( ppos ) , param )
1024
1039
|
1025
1040
exists ( Guard g0 , GuardValue v0 |
1026
1041
g0 .directlyValueControls ( ret .getBasicBlock ( ) , v0 ) and
1027
1042
BranchImplies:: ssaControls ( param , val , g0 , v0 ) and
1028
- retval = [ true , false ]
1043
+ relevantReturnValue ( m , retval )
1029
1044
)
1030
1045
or
1031
- ReturnImplies:: ssaControls ( param , val , ret ,
1032
- any ( GuardValue r | r .asBooleanValue ( ) = retval ) )
1046
+ ReturnImplies:: ssaControls ( param , val , ret , retval )
1033
1047
)
1034
1048
}
1035
1049
1036
1050
/**
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
1039
1053
* that the argument has the value `val`.
1040
1054
*/
1041
- private BooleanMethod customGuard ( ParameterPosition ppos , boolean retval , GuardValue val ) {
1055
+ private NonOverridableMethod customGuard (
1056
+ ParameterPosition ppos , GuardValue retval , GuardValue val
1057
+ ) {
1042
1058
forex ( ReturnExpr ret |
1043
1059
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
+ )
1045
1064
|
1046
1065
validReturnInCustomGuard ( ret , ppos , retval , val )
1047
1066
)
@@ -1056,11 +1075,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1056
1075
* custom guard wrappers.
1057
1076
*/
1058
1077
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 |
1060
1079
g1 = call and
1061
- call .getMethod ( ) = customGuard ( ppos , v1 . asBooleanValue ( ) , v2 ) and
1080
+ call .getMethod ( ) = customGuard ( ppos , v1 , v2 ) and
1062
1081
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
1064
1084
)
1065
1085
}
1066
1086
}
0 commit comments