@@ -1283,36 +1283,35 @@ module Make<
12831283 signature predicate guardChecksSig ( Guard g , Expr e , GuardValue gv ) ;
12841284
12851285 bindingset [ this ]
1286- signature class StateSig ;
1286+ signature class ParamSig ;
12871287
1288- private module WithState < StateSig State > {
1289- signature predicate guardChecksSig ( Guard g , Expr e , GuardValue gv , State state ) ;
1288+ private module WithParam < ParamSig P > {
1289+ signature predicate guardChecksSig ( Guard g , Expr e , GuardValue gv , P par ) ;
12901290 }
12911291
12921292 /**
12931293 * Extends a `BarrierGuard` input predicate with wrapped invocations.
12941294 */
12951295 module ValidationWrapper< guardChecksSig / 3 guardChecks0> {
1296- private predicate guardChecksWithState ( Guard g , Expr e , GuardValue gv , Unit state ) {
1297- guardChecks0 ( g , e , gv ) and exists ( state )
1296+ private predicate guardChecksWithParam ( Guard g , Expr e , GuardValue gv , Unit par ) {
1297+ guardChecks0 ( g , e , gv ) and exists ( par )
12981298 }
12991299
1300- private module StatefulWrapper = ValidationWrapperWithState< Unit , guardChecksWithState / 4 > ;
1300+ private module ParameterizedWrapper =
1301+ ParameterizedValidationWrapper< Unit , guardChecksWithParam / 4 > ;
13011302
13021303 /**
13031304 * Holds if the guard `g` validates the SSA definition `def` upon evaluating to `val`.
13041305 */
13051306 predicate guardChecksDef ( Guard g , SsaDefinition def , GuardValue val ) {
1306- StatefulWrapper :: guardChecksDef ( g , def , val , _)
1307+ ParameterizedWrapper :: guardChecksDef ( g , def , val , _)
13071308 }
13081309 }
13091310
13101311 /**
13111312 * Extends a `BarrierGuard` input predicate with wrapped invocations.
13121313 */
1313- module ValidationWrapperWithState<
1314- StateSig State, WithState< State > :: guardChecksSig / 4 guardChecks0>
1315- {
1314+ module ParameterizedValidationWrapper< ParamSig P, WithParam< P > :: guardChecksSig / 4 guardChecks0> {
13161315 private import WrapperGuard
13171316
13181317 /**
@@ -1321,12 +1320,12 @@ module Make<
13211320 * parameter has been validated by the given guard.
13221321 */
13231322 private predicate validReturnInValidationWrapper (
1324- ReturnExpr ret , ParameterPosition ppos , GuardValue retval , State state
1323+ ReturnExpr ret , ParameterPosition ppos , GuardValue retval , P par
13251324 ) {
13261325 exists ( NonOverridableMethod m , SsaParameterInit param , Guard guard , GuardValue val |
13271326 m .getAReturnExpr ( ) = ret and
13281327 param .getParameter ( ) = m .getParameter ( ppos ) and
1329- guardChecksDef ( guard , param , val , state )
1328+ guardChecksDef ( guard , param , val , par )
13301329 |
13311330 guard .valueControls ( ret .getBasicBlock ( ) , val ) and
13321331 relevantReturnExprValue ( m , ret , retval )
@@ -1341,7 +1340,7 @@ module Make<
13411340 * that the argument has been validated by the given guard.
13421341 */
13431342 private NonOverridableMethod validationWrapper (
1344- ParameterPosition ppos , GuardValue retval , State state
1343+ ParameterPosition ppos , GuardValue retval , P par
13451344 ) {
13461345 forex ( ReturnExpr ret |
13471346 result .getAReturnExpr ( ) = ret and
@@ -1350,12 +1349,12 @@ module Make<
13501349 disjointValues ( notRetval , retval )
13511350 )
13521351 |
1353- validReturnInValidationWrapper ( ret , ppos , retval , state )
1352+ validReturnInValidationWrapper ( ret , ppos , retval , par )
13541353 )
13551354 or
13561355 exists ( SsaParameterInit param , BasicBlock bb , Guard guard , GuardValue val |
13571356 param .getParameter ( ) = result .getParameter ( ppos ) and
1358- guardChecksDef ( guard , param , val , state ) and
1357+ guardChecksDef ( guard , param , val , par ) and
13591358 guard .valueControls ( bb , val ) and
13601359 normalExitBlock ( bb ) and
13611360 retval = TException ( false )
@@ -1365,12 +1364,12 @@ module Make<
13651364 /**
13661365 * Holds if the guard `g` validates the expression `e` upon evaluating to `val`.
13671366 */
1368- private predicate guardChecks ( Guard g , Expr e , GuardValue val , State state ) {
1369- guardChecks0 ( g , e , val , state )
1367+ private predicate guardChecks ( Guard g , Expr e , GuardValue val , P par ) {
1368+ guardChecks0 ( g , e , val , par )
13701369 or
13711370 exists ( NonOverridableMethodCall call , ParameterPosition ppos , ArgumentPosition apos |
13721371 g = call and
1373- call .getMethod ( ) = validationWrapper ( ppos , val , state ) and
1372+ call .getMethod ( ) = validationWrapper ( ppos , val , par ) and
13741373 call .getArgument ( apos ) = e and
13751374 parameterMatch ( pragma [ only_bind_out ] ( ppos ) , pragma [ only_bind_out ] ( apos ) )
13761375 )
@@ -1379,9 +1378,9 @@ module Make<
13791378 /**
13801379 * Holds if the guard `g` validates the SSA definition `def` upon evaluating to `val`.
13811380 */
1382- predicate guardChecksDef ( Guard g , SsaDefinition def , GuardValue val , State state ) {
1381+ predicate guardChecksDef ( Guard g , SsaDefinition def , GuardValue val , P par ) {
13831382 exists ( Expr e |
1384- guardChecks ( g , e , val , state ) and
1383+ guardChecks ( g , e , val , par ) and
13851384 guardReadsSsaVar ( e , def )
13861385 )
13871386 }
0 commit comments