@@ -52,6 +52,7 @@ module;
5252
5353private import codeql.util.Boolean
5454private import codeql.util.Location
55+ private import codeql.util.Unit
5556
5657signature module InputSig< LocationSig Location> {
5758 class SuccessorType {
@@ -1002,7 +1003,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
10021003 private module WrapperGuard {
10031004 final private class FinalExpr = Expr ;
10041005
1005- private class ReturnExpr extends FinalExpr {
1006+ class ReturnExpr extends FinalExpr {
10061007 ReturnExpr ( ) { any ( NonOverridableMethod m ) .getAReturnExpr ( ) = this }
10071008
10081009 NonOverridableMethod getMethod ( ) { result .getAReturnExpr ( ) = this }
@@ -1016,7 +1017,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
10161017 ReturnImplies:: guardControls ( call , val , _, _)
10171018 }
10181019
1019- private predicate relevantReturnValue ( NonOverridableMethod m , GuardValue val ) {
1020+ predicate relevantReturnValue ( NonOverridableMethod m , GuardValue val ) {
10201021 exists ( NonOverridableMethodCall call |
10211022 relevantCallValue ( call , val ) and
10221023 call .getMethod ( ) = m and
@@ -1028,7 +1029,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
10281029 relevantReturnValue ( guard .( ReturnExpr ) .getMethod ( ) , val )
10291030 }
10301031
1031- private module ReturnImplies = ImpliesTC< returnGuard / 2 > ;
1032+ module ReturnImplies = ImpliesTC< returnGuard / 2 > ;
10321033
10331034 /**
10341035 * Holds if `ret` is a return expression in a non-overridable method that
@@ -1104,6 +1105,103 @@ module Make<LocationSig Location, InputSig<Location> Input> {
11041105 }
11051106 }
11061107
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+
11071205 /**
11081206 * A guard. This may be any expression whose value determines subsequent
11091207 * control flow. It may also be a switch case, which as a guard is considered
0 commit comments