@@ -207,6 +207,46 @@ signature module InputSig<LocationSig Location> {
207
207
/** Gets the false branch of this expression. */
208
208
Expr getElse ( ) ;
209
209
}
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
+ }
210
250
}
211
251
212
252
/** Provides guards-related predicates and classes. */
@@ -503,6 +543,8 @@ module Make<LocationSig Location, InputSig<Location> Input> {
503
543
predicate hasInputFromBlock ( SsaDefinition inp , BasicBlock bb ) ;
504
544
}
505
545
546
+ predicate parameterDefinition ( Parameter p , SsaDefinition def ) ;
547
+
506
548
/**
507
549
* Holds if `guard` evaluating to `val` ensures that:
508
550
* `e <= k` when `upper = true`
@@ -525,8 +567,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
525
567
* Holds if the assumption that `g1` has been evaluated to `v1` implies that
526
568
* `g2` has been evaluated to `v2`, that is, the evaluation of `g2` to `v2`
527
569
* dominates the evaluation of `g1` to `v1`.
528
- *
529
- * This predicate can be instantiated with `CustomGuard<..>::additionalImpliesStep`.
530
570
*/
531
571
default predicate additionalImpliesStep ( PreGuard g1 , GuardValue v1 , PreGuard g2 , GuardValue v2 ) {
532
572
none ( )
@@ -859,6 +899,11 @@ module Make<LocationSig Location, InputSig<Location> Input> {
859
899
impliesStepSsaGuard ( def0 , v0 , guard , v )
860
900
)
861
901
or
902
+ exists ( Guard g0 , GuardValue v0 |
903
+ guardControls ( g0 , v0 , tgtGuard , tgtVal ) and
904
+ CustomGuard:: additionalImpliesStep ( g0 , v0 , guard , v )
905
+ )
906
+ or
862
907
exists ( Guard g0 , GuardValue v0 |
863
908
guardControls ( g0 , v0 , tgtGuard , tgtVal ) and
864
909
additionalImpliesStep ( g0 , v0 , guard , v )
@@ -902,6 +947,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
902
947
*/
903
948
predicate nullGuard ( Guard guard , GuardValue v , Expr e , boolean isNull ) {
904
949
impliesStep2 ( guard , v , e , any ( GuardValue gv | gv .isNullness ( isNull ) ) ) or
950
+ CustomGuard:: additionalImpliesStep ( guard , v , e , any ( GuardValue gv | gv .isNullness ( isNull ) ) ) or
905
951
additionalImpliesStep ( guard , v , e , any ( GuardValue gv | gv .isNullness ( isNull ) ) )
906
952
}
907
953
@@ -944,47 +990,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
944
990
)
945
991
}
946
992
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
-
980
993
/**
981
994
* Provides an implementation of guard implication logic for custom
982
995
* wrappers. This can be used to instantiate the `additionalImpliesStep`
983
996
* predicate.
984
997
*/
985
- module CustomGuard< CustomGuardInputSig CustomGuardInput> {
986
- private import CustomGuardInput
987
-
998
+ private module CustomGuard {
988
999
final private class FinalExpr = Expr ;
989
1000
990
1001
private class ReturnExpr extends FinalExpr {
@@ -1010,7 +1021,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1010
1021
) {
1011
1022
exists ( BooleanMethod m , SsaDefinition param |
1012
1023
m .getAReturnExpr ( ) = ret and
1013
- m .getParameter ( ppos ) = param
1024
+ parameterDefinition ( m .getParameter ( ppos ) , param )
1014
1025
|
1015
1026
exists ( Guard g0 , GuardValue v0 |
1016
1027
g0 .directlyValueControls ( ret .getBasicBlock ( ) , v0 ) and
0 commit comments