@@ -258,13 +258,13 @@ private class MaxValueState extends TMaxValueState {
258
258
* A node that blocks some flow states and transforms some others as they flow
259
259
* through it.
260
260
*/
261
- abstract class BarrierFlowStateTransformer extends DataFlow:: Node {
261
+ abstract class FlowStateTransformer extends DataFlow:: Node {
262
262
/**
263
263
* Holds if this should be a barrier for `flowstate`.
264
264
*
265
265
* This includes flow states which are transformed into other flow states.
266
266
*/
267
- abstract predicate barrierFor ( MaxValueState flowstate ) ;
267
+ abstract predicate barrierFor ( int bitSize , int architectureBitSize ) ;
268
268
269
269
/**
270
270
* Gets the flow state that `flowstate` is transformed into.
@@ -275,7 +275,20 @@ abstract class BarrierFlowStateTransformer extends DataFlow::Node {
275
275
* transform(transform(x)) = transform(x)
276
276
* ```
277
277
*/
278
- abstract MaxValueState transform ( MaxValueState flowstate ) ;
278
+ MaxValueState transform ( MaxValueState state ) {
279
+ this .barrierFor ( state .getBitSize ( ) , state .getSinkBitSize ( ) ) and
280
+ result .getBitSize ( ) =
281
+ max ( int bitsize |
282
+ bitsize = validBitSize ( ) and
283
+ bitsize < state .getBitSize ( ) and
284
+ not this .barrierFor ( bitsize , state .getSinkBitSize ( ) )
285
+ ) and
286
+ (
287
+ result .getArchitectureBitSize ( ) = state .getArchitectureBitSize ( )
288
+ or
289
+ state .architectureBitSizeUnknown ( ) and result .architectureBitSizeUnknown ( )
290
+ )
291
+ }
279
292
}
280
293
281
294
private predicate upperBoundCheckGuard ( DataFlow:: Node g , Expr e , boolean branch ) {
@@ -372,30 +385,15 @@ class UpperBoundCheckGuard extends DataFlow::RelationalComparisonNode {
372
385
* for all flow states and would not transform any flow states, thus
373
386
* effectively blocking them.
374
387
*/
375
- class UpperBoundCheck extends BarrierFlowStateTransformer {
388
+ class UpperBoundCheck extends FlowStateTransformer {
376
389
UpperBoundCheckGuard g ;
377
390
378
391
UpperBoundCheck ( ) {
379
392
this = DataFlow:: BarrierGuard< upperBoundCheckGuard / 3 > :: getABarrierNodeForGuard ( g )
380
393
}
381
394
382
- override predicate barrierFor ( MaxValueState flowstate ) {
383
- g .isBoundFor ( flowstate .getBitSize ( ) , flowstate .getSinkBitSize ( ) )
384
- }
385
-
386
- override MaxValueState transform ( MaxValueState state ) {
387
- this .barrierFor ( state ) and
388
- result .getBitSize ( ) =
389
- max ( int bitsize |
390
- bitsize = validBitSize ( ) and
391
- bitsize < state .getBitSize ( ) and
392
- not g .isBoundFor ( bitsize , state .getSinkBitSize ( ) )
393
- ) and
394
- (
395
- result .getArchitectureBitSize ( ) = state .getArchitectureBitSize ( )
396
- or
397
- state .architectureBitSizeUnknown ( ) and result .architectureBitSizeUnknown ( )
398
- )
395
+ override predicate barrierFor ( int bitSize , int architectureBitSize ) {
396
+ g .isBoundFor ( bitSize , architectureBitSize )
399
397
}
400
398
}
401
399
@@ -497,7 +495,10 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
497
495
498
496
predicate isBarrier ( DataFlow:: Node node , FlowState state ) {
499
497
// Safely guarded by a barrier guard.
500
- exists ( BarrierFlowStateTransformer bfst | node = bfst and bfst .barrierFor ( state ) )
498
+ exists ( FlowStateTransformer fst |
499
+ node = fst and
500
+ fst .barrierFor ( state .getBitSize ( ) , state .getSinkBitSize ( ) )
501
+ )
501
502
or
502
503
// When there is a flow from a source to a sink, do not allow the flow to
503
504
// continue to a further sink.
@@ -507,8 +508,8 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
507
508
predicate isAdditionalFlowStep (
508
509
DataFlow:: Node node1 , FlowState state1 , DataFlow:: Node node2 , FlowState state2
509
510
) {
510
- // Create additional flow steps for `BarrierFlowStateTransformer `s
511
- state2 = node2 .( BarrierFlowStateTransformer ) .transform ( state1 ) and
511
+ // Create additional flow steps for `FlowStateTransformer `s
512
+ state2 = node2 .( FlowStateTransformer ) .transform ( state1 ) and
512
513
DataFlow:: simpleLocalFlowStep ( node1 , node2 , _)
513
514
}
514
515
}
0 commit comments