@@ -52,6 +52,7 @@ module;
52
52
53
53
private import codeql.util.Boolean
54
54
private import codeql.util.Location
55
+ private import codeql.util.Unit
55
56
56
57
signature module InputSig< LocationSig Location> {
57
58
class SuccessorType {
@@ -1009,7 +1010,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1009
1010
private module WrapperGuard {
1010
1011
final private class FinalExpr = Expr ;
1011
1012
1012
- private class ReturnExpr extends FinalExpr {
1013
+ class ReturnExpr extends FinalExpr {
1013
1014
ReturnExpr ( ) { any ( NonOverridableMethod m ) .getAReturnExpr ( ) = this }
1014
1015
1015
1016
NonOverridableMethod getMethod ( ) { result .getAReturnExpr ( ) = this }
@@ -1023,7 +1024,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1023
1024
ReturnImplies:: guardControls ( call , val , _, _)
1024
1025
}
1025
1026
1026
- private predicate relevantReturnValue ( NonOverridableMethod m , GuardValue val ) {
1027
+ predicate relevantReturnValue ( NonOverridableMethod m , GuardValue val ) {
1027
1028
exists ( NonOverridableMethodCall call |
1028
1029
relevantCallValue ( call , val ) and
1029
1030
call .getMethod ( ) = m and
@@ -1035,7 +1036,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1035
1036
relevantReturnValue ( guard .( ReturnExpr ) .getMethod ( ) , val )
1036
1037
}
1037
1038
1038
- private module ReturnImplies = ImpliesTC< returnGuard / 2 > ;
1039
+ module ReturnImplies = ImpliesTC< returnGuard / 2 > ;
1039
1040
1040
1041
/**
1041
1042
* Holds if `ret` is a return expression in a non-overridable method that
@@ -1113,6 +1114,105 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1113
1114
}
1114
1115
}
1115
1116
1117
+ signature predicate guardChecksSig ( Guard g , Expr e , boolean branch ) ;
1118
+
1119
+ bindingset [ this ]
1120
+ signature class StateSig ;
1121
+
1122
+ private module WithState< StateSig State> {
1123
+ signature predicate guardChecksSig ( Guard g , Expr e , boolean branch , State state ) ;
1124
+ }
1125
+
1126
+ /**
1127
+ * Extends a `BarrierGuard` input predicate with wrapped invocations.
1128
+ */
1129
+ module ValidationWrapper< guardChecksSig / 3 guardChecks0> {
1130
+ private predicate guardChecksWithState ( Guard g , Expr e , boolean branch , Unit state ) {
1131
+ guardChecks0 ( g , e , branch ) and exists ( state )
1132
+ }
1133
+
1134
+ private module StatefulWrapper = ValidationWrapperWithState< Unit , guardChecksWithState / 4 > ;
1135
+
1136
+ /**
1137
+ * Holds if the guard `g` validates the expression `e` upon evaluating to `val`.
1138
+ */
1139
+ predicate guardChecks ( Guard g , Expr e , GuardValue val ) {
1140
+ StatefulWrapper:: guardChecks ( g , e , val , _)
1141
+ }
1142
+ }
1143
+
1144
+ /**
1145
+ * Extends a `BarrierGuard` input predicate with wrapped invocations.
1146
+ */
1147
+ module ValidationWrapperWithState<
1148
+ StateSig State, WithState< State > :: guardChecksSig / 4 guardChecks0>
1149
+ {
1150
+ private import WrapperGuard
1151
+
1152
+ /**
1153
+ * Holds if `ret` is a return expression in a non-overridable method that
1154
+ * on a return value of `retval` allows the conclusion that the `ppos`th
1155
+ * parameter has been validated by the given guard.
1156
+ */
1157
+ private predicate validReturnInValidationWrapper (
1158
+ ReturnExpr ret , ParameterPosition ppos , GuardValue retval , State state
1159
+ ) {
1160
+ exists ( NonOverridableMethod m , SsaDefinition param , Guard guard , GuardValue val |
1161
+ m .getAReturnExpr ( ) = ret and
1162
+ parameterDefinition ( m .getParameter ( ppos ) , param ) and
1163
+ guardChecks ( guard , param .getARead ( ) , val , state )
1164
+ |
1165
+ guard .valueControls ( ret .getBasicBlock ( ) , val ) and
1166
+ relevantReturnValue ( m , retval )
1167
+ or
1168
+ ReturnImplies:: guardControls ( guard , val , ret , retval )
1169
+ )
1170
+ }
1171
+
1172
+ /**
1173
+ * Gets a non-overridable method that performs a check on the `ppos`th
1174
+ * parameter. A return value equal to `retval` allows us to conclude
1175
+ * that the argument has been validated by the given guard.
1176
+ */
1177
+ private NonOverridableMethod validationWrapper (
1178
+ ParameterPosition ppos , GuardValue retval , State state
1179
+ ) {
1180
+ forex ( ReturnExpr ret |
1181
+ result .getAReturnExpr ( ) = ret and
1182
+ not exists ( GuardValue notRetval |
1183
+ exprHasValue ( ret , notRetval ) and
1184
+ disjointValues ( notRetval , retval )
1185
+ )
1186
+ |
1187
+ validReturnInValidationWrapper ( ret , ppos , retval , state )
1188
+ )
1189
+ or
1190
+ exists ( SsaDefinition param , BasicBlock bb , Guard guard , GuardValue val |
1191
+ parameterDefinition ( result .getParameter ( ppos ) , param ) and
1192
+ guardChecks ( guard , param .getARead ( ) , val , state ) and
1193
+ guard .valueControls ( bb , val )
1194
+ |
1195
+ normalExitBlock ( bb ) and retval = TException ( false )
1196
+ or
1197
+ exceptionalExitBlock ( bb ) and retval = TException ( true )
1198
+ )
1199
+ }
1200
+
1201
+ /**
1202
+ * Holds if the guard `g` validates the expression `e` upon evaluating to `val`.
1203
+ */
1204
+ predicate guardChecks ( Guard g , Expr e , GuardValue val , State state ) {
1205
+ guardChecks0 ( g , e , val .asBooleanValue ( ) , state )
1206
+ or
1207
+ exists ( NonOverridableMethodCall call , ParameterPosition ppos , ArgumentPosition apos |
1208
+ g = call and
1209
+ call .getMethod ( ) = validationWrapper ( ppos , val , state ) and
1210
+ call .getArgument ( apos ) = e and
1211
+ parameterMatch ( pragma [ only_bind_out ] ( ppos ) , pragma [ only_bind_out ] ( apos ) )
1212
+ )
1213
+ }
1214
+ }
1215
+
1116
1216
/**
1117
1217
* A guard. This may be any expression whose value determines subsequent
1118
1218
* control flow. It may also be a switch case, which as a guard is considered
0 commit comments