@@ -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 {
@@ -1002,7 +1003,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1002
1003
private module WrapperGuard {
1003
1004
final private class FinalExpr = Expr ;
1004
1005
1005
- private class ReturnExpr extends FinalExpr {
1006
+ class ReturnExpr extends FinalExpr {
1006
1007
ReturnExpr ( ) { any ( NonOverridableMethod m ) .getAReturnExpr ( ) = this }
1007
1008
1008
1009
NonOverridableMethod getMethod ( ) { result .getAReturnExpr ( ) = this }
@@ -1016,7 +1017,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1016
1017
ReturnImplies:: guardControls ( call , val , _, _)
1017
1018
}
1018
1019
1019
- private predicate relevantReturnValue ( NonOverridableMethod m , GuardValue val ) {
1020
+ predicate relevantReturnValue ( NonOverridableMethod m , GuardValue val ) {
1020
1021
exists ( NonOverridableMethodCall call |
1021
1022
relevantCallValue ( call , val ) and
1022
1023
call .getMethod ( ) = m and
@@ -1028,7 +1029,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1028
1029
relevantReturnValue ( guard .( ReturnExpr ) .getMethod ( ) , val )
1029
1030
}
1030
1031
1031
- private module ReturnImplies = ImpliesTC< returnGuard / 2 > ;
1032
+ module ReturnImplies = ImpliesTC< returnGuard / 2 > ;
1032
1033
1033
1034
/**
1034
1035
* Holds if `ret` is a return expression in a non-overridable method that
@@ -1104,6 +1105,103 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1104
1105
}
1105
1106
}
1106
1107
1108
+ signature predicate guardChecksSig ( Guard g , Expr e , boolean branch ) ;
1109
+
1110
+ bindingset [ this ]
1111
+ signature class StateSig ;
1112
+
1113
+ private module WithState< StateSig State> {
1114
+ signature predicate guardChecksSig ( Guard g , Expr e , boolean branch , State state ) ;
1115
+ }
1116
+
1117
+ /**
1118
+ * Extends a `BarrierGuard` input predicate with wrapped invocations.
1119
+ */
1120
+ module ValidationWrapper< guardChecksSig / 3 guardChecks0> {
1121
+ private predicate guardChecksWithState ( Guard g , Expr e , boolean branch , Unit state ) {
1122
+ guardChecks0 ( g , e , branch ) and exists ( state )
1123
+ }
1124
+
1125
+ private module StatefulWrapper = ValidationWrapperWithState< Unit , guardChecksWithState / 4 > ;
1126
+
1127
+ /**
1128
+ * Holds if the guard `g` validates the expression `e` upon evaluating to `val`.
1129
+ */
1130
+ predicate guardChecks ( Guard g , Expr e , GuardValue val ) {
1131
+ StatefulWrapper:: guardChecks ( g , e , val , _)
1132
+ }
1133
+ }
1134
+
1135
+ /**
1136
+ * Extends a `BarrierGuard` input predicate with wrapped invocations.
1137
+ */
1138
+ module ValidationWrapperWithState<
1139
+ StateSig State, WithState< State > :: guardChecksSig / 4 guardChecks0>
1140
+ {
1141
+ private import WrapperGuard
1142
+
1143
+ /**
1144
+ * Holds if `ret` is a return expression in a non-overridable method that
1145
+ * on a return value of `retval` allows the conclusion that the `ppos`th
1146
+ * parameter has been validated by the given guard.
1147
+ */
1148
+ private predicate validReturnInValidationWrapper (
1149
+ ReturnExpr ret , ParameterPosition ppos , GuardValue retval , State state
1150
+ ) {
1151
+ exists ( NonOverridableMethod m , SsaDefinition param , Guard guard , GuardValue val |
1152
+ m .getAReturnExpr ( ) = ret and
1153
+ parameterDefinition ( m .getParameter ( ppos ) , param ) and
1154
+ guardChecks ( guard , param .getARead ( ) , val , state )
1155
+ |
1156
+ guard .valueControls ( ret .getBasicBlock ( ) , val ) and
1157
+ relevantReturnValue ( m , retval )
1158
+ or
1159
+ ReturnImplies:: guardControls ( guard , val , ret , retval )
1160
+ )
1161
+ }
1162
+
1163
+ /**
1164
+ * Gets a non-overridable method that performs a check on the `ppos`th
1165
+ * parameter. A return value equal to `retval` allows us to conclude
1166
+ * that the argument has been validated by the given guard.
1167
+ */
1168
+ private NonOverridableMethod validationWrapper (
1169
+ ParameterPosition ppos , GuardValue retval , State state
1170
+ ) {
1171
+ forex ( ReturnExpr ret |
1172
+ result .getAReturnExpr ( ) = ret and
1173
+ not exists ( GuardValue notRetval |
1174
+ exprHasValue ( ret , notRetval ) and
1175
+ disjointValues ( notRetval , retval )
1176
+ )
1177
+ |
1178
+ validReturnInValidationWrapper ( ret , ppos , retval , state )
1179
+ )
1180
+ or
1181
+ exists ( SsaDefinition param , BasicBlock bb , Guard guard , GuardValue val |
1182
+ parameterDefinition ( result .getParameter ( ppos ) , param ) and
1183
+ guardChecks ( guard , param .getARead ( ) , val , state ) and
1184
+ guard .valueControls ( bb , val ) and
1185
+ normalExitBlock ( bb ) and
1186
+ retval = TException ( false )
1187
+ )
1188
+ }
1189
+
1190
+ /**
1191
+ * Holds if the guard `g` validates the expression `e` upon evaluating to `val`.
1192
+ */
1193
+ predicate guardChecks ( Guard g , Expr e , GuardValue val , State state ) {
1194
+ guardChecks0 ( g , e , val .asBooleanValue ( ) , state )
1195
+ or
1196
+ exists ( NonOverridableMethodCall call , ParameterPosition ppos , ArgumentPosition apos |
1197
+ g = call and
1198
+ call .getMethod ( ) = validationWrapper ( ppos , val , state ) and
1199
+ call .getArgument ( apos ) = e and
1200
+ parameterMatch ( pragma [ only_bind_out ] ( ppos ) , pragma [ only_bind_out ] ( apos ) )
1201
+ )
1202
+ }
1203
+ }
1204
+
1107
1205
/**
1108
1206
* A guard. This may be any expression whose value determines subsequent
1109
1207
* control flow. It may also be a switch case, which as a guard is considered
0 commit comments