@@ -207,6 +207,46 @@ signature module InputSig<LocationSig Location> {
207207 /** Gets the false branch of this expression. */
208208 Expr getElse ( ) ;
209209 }
210+
211+ class Parameter {
212+ /** Gets a textual representation of this parameter. */
213+ string toString ( ) ;
214+
215+ /** Gets the location of this parameter. */
216+ Location getLocation ( ) ;
217+ }
218+
219+ class ParameterPosition {
220+ /** Gets a textual representation of this element. */
221+ bindingset [ this ]
222+ string toString ( ) ;
223+ }
224+
225+ class ArgumentPosition {
226+ /** Gets a textual representation of this element. */
227+ bindingset [ this ]
228+ string toString ( ) ;
229+ }
230+
231+ /**
232+ * Holds if the parameter position `ppos` matches the argument position
233+ * `apos`.
234+ */
235+ predicate parameterMatch ( ParameterPosition ppos , ArgumentPosition apos ) ;
236+
237+ /** A non-overridable method with a boolean return value. */
238+ class BooleanMethod {
239+ Parameter getParameter ( ParameterPosition ppos ) ;
240+
241+ /** Gets an expression being returned by this method. */
242+ Expr getAReturnExpr ( ) ;
243+ }
244+
245+ class BooleanMethodCall extends Expr {
246+ BooleanMethod getMethod ( ) ;
247+
248+ Expr getArgument ( ArgumentPosition apos ) ;
249+ }
210250}
211251
212252/** Provides guards-related predicates and classes. */
@@ -503,6 +543,8 @@ module Make<LocationSig Location, InputSig<Location> Input> {
503543 predicate hasInputFromBlock ( SsaDefinition inp , BasicBlock bb ) ;
504544 }
505545
546+ predicate parameterDefinition ( Parameter p , SsaDefinition def ) ;
547+
506548 /**
507549 * Holds if `guard` evaluating to `val` ensures that:
508550 * `e <= k` when `upper = true`
@@ -525,8 +567,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
525567 * Holds if the assumption that `g1` has been evaluated to `v1` implies that
526568 * `g2` has been evaluated to `v2`, that is, the evaluation of `g2` to `v2`
527569 * dominates the evaluation of `g1` to `v1`.
528- *
529- * This predicate can be instantiated with `CustomGuard<..>::additionalImpliesStep`.
530570 */
531571 default predicate additionalImpliesStep ( PreGuard g1 , GuardValue v1 , PreGuard g2 , GuardValue v2 ) {
532572 none ( )
@@ -859,6 +899,11 @@ module Make<LocationSig Location, InputSig<Location> Input> {
859899 impliesStepSsaGuard ( def0 , v0 , guard , v )
860900 )
861901 or
902+ exists ( Guard g0 , GuardValue v0 |
903+ guardControls ( g0 , v0 , tgtGuard , tgtVal ) and
904+ CustomGuard:: additionalImpliesStep ( g0 , v0 , guard , v )
905+ )
906+ or
862907 exists ( Guard g0 , GuardValue v0 |
863908 guardControls ( g0 , v0 , tgtGuard , tgtVal ) and
864909 additionalImpliesStep ( g0 , v0 , guard , v )
@@ -902,6 +947,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
902947 */
903948 predicate nullGuard ( Guard guard , GuardValue v , Expr e , boolean isNull ) {
904949 impliesStep2 ( guard , v , e , any ( GuardValue gv | gv .isNullness ( isNull ) ) ) or
950+ CustomGuard:: additionalImpliesStep ( guard , v , e , any ( GuardValue gv | gv .isNullness ( isNull ) ) ) or
905951 additionalImpliesStep ( guard , v , e , any ( GuardValue gv | gv .isNullness ( isNull ) ) )
906952 }
907953
@@ -944,47 +990,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
944990 )
945991 }
946992
947- signature module CustomGuardInputSig {
948- class ParameterPosition {
949- /** Gets a textual representation of this element. */
950- bindingset [ this ]
951- string toString ( ) ;
952- }
953-
954- class ArgumentPosition {
955- /** Gets a textual representation of this element. */
956- bindingset [ this ]
957- string toString ( ) ;
958- }
959-
960- /**
961- * Holds if the parameter position `ppos` matches the argument position
962- * `apos`.
963- */
964- predicate parameterMatch ( ParameterPosition ppos , ArgumentPosition apos ) ;
965-
966- /** A non-overridable method with a boolean return value. */
967- class BooleanMethod {
968- SsaDefinition getParameter ( ParameterPosition ppos ) ;
969-
970- Expr getAReturnExpr ( ) ;
971- }
972-
973- class BooleanMethodCall extends Expr {
974- BooleanMethod getMethod ( ) ;
975-
976- Expr getArgument ( ArgumentPosition apos ) ;
977- }
978- }
979-
980993 /**
981994 * Provides an implementation of guard implication logic for custom
982995 * wrappers. This can be used to instantiate the `additionalImpliesStep`
983996 * predicate.
984997 */
985- module CustomGuard< CustomGuardInputSig CustomGuardInput> {
986- private import CustomGuardInput
987-
998+ private module CustomGuard {
988999 final private class FinalExpr = Expr ;
9891000
9901001 private class ReturnExpr extends FinalExpr {
@@ -1010,7 +1021,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
10101021 ) {
10111022 exists ( BooleanMethod m , SsaDefinition param |
10121023 m .getAReturnExpr ( ) = ret and
1013- m .getParameter ( ppos ) = param
1024+ parameterDefinition ( m .getParameter ( ppos ) , param )
10141025 |
10151026 exists ( Guard g0 , GuardValue v0 |
10161027 g0 .directlyValueControls ( ret .getBasicBlock ( ) , v0 ) and
0 commit comments