@@ -88,20 +88,39 @@ class StdlibRandomSource extends RandomDataSource {
88
88
m .getDeclaringType ( ) instanceof StdlibRandom
89
89
}
90
90
91
+ // Note for the following bounds functions: `java.util.Random` only defines no-arg versions
92
+ // of `nextInt` and `nextLong` plus `nextInt(int x)`, bounded to the range [0, x)
93
+ // However `ThreadLocalRandom` provides one- and two-arg versions of `nextInt` and `nextLong`
94
+ // which allow both lower and upper bounds for both types.
91
95
override int getLowerBound ( ) {
92
- // If this call is to `nextInt(int)`, the lower bound is zero.
93
- m .hasName ( "nextInt" ) and
96
+ // If this call is to `nextInt(int)` or `nextLong(long) , the lower bound is zero.
97
+ m .hasName ( [ "nextInt" , "nextLong" ] ) and
94
98
m .getNumberOfParameters ( ) = 1 and
95
99
result = 0
100
+ or
101
+ result = super .getLowerBound ( ) // Include a lower bound provided via `getLowerBoundExpr`
96
102
}
97
103
98
- override Expr getUpperBoundExpr ( ) {
99
- // If this call is to `nextInt(int)`, the upper bound is the first argument.
100
- m .hasName ( "nextInt" ) and
101
- m .getNumberOfParameters ( ) = 1 and
104
+ override Expr getLowerBoundExpr ( ) {
105
+ // If this call is to `nextInt(int, int)` or `nextLong(long, long)`, the lower bound is the first argument.
106
+ m .hasName ( [ "nextInt" , "nextLong" ] ) and
107
+ m .getNumberOfParameters ( ) = 2 and
102
108
result = this .getArgument ( 0 )
103
109
}
104
110
111
+ override Expr getUpperBoundExpr ( ) {
112
+ // If this call is to `nextInt(int)` or `nextLong(long)`, the upper bound is the first argument.
113
+ // If it calls `nextInt(int, int)` or `nextLong(long, long)`, the upper bound is the first argument.
114
+ m .hasName ( [ "nextInt" , "nextLong" ] ) and
115
+ (
116
+ m .getNumberOfParameters ( ) = 1 and
117
+ result = this .getArgument ( 0 )
118
+ or
119
+ m .getNumberOfParameters ( ) = 2 and
120
+ result = this .getArgument ( 1 )
121
+ )
122
+ }
123
+
105
124
override predicate resultMayBeBounded ( ) {
106
125
// `next` may be restricted by its `bits` argument,
107
126
// `nextBoolean` can't possibly be usefully bounded,
@@ -110,7 +129,7 @@ class StdlibRandomSource extends RandomDataSource {
110
129
m .hasName ( [ "next" , "nextBoolean" , "nextDouble" , "nextFloat" , "nextGaussian" ] )
111
130
or
112
131
m .hasName ( [ "nextInt" , "nextLong" ] ) and
113
- m .getNumberOfParameters ( ) = 1
132
+ m .getNumberOfParameters ( ) = [ 1 , 2 ]
114
133
}
115
134
116
135
override Expr getOutput ( ) {
0 commit comments