@@ -258,13 +258,14 @@ 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
- * Holds if this should be a barrier for `flowstate`.
263
+ * Holds if this should be a barrier for a flow state with bit size `bitSize`
264
+ * and architecture bit size `architectureBitSize`.
264
265
*
265
266
* This includes flow states which are transformed into other flow states.
266
267
*/
267
- abstract predicate barrierFor ( MaxValueState flowstate ) ;
268
+ abstract predicate barrierFor ( int bitSize , int architectureBitSize ) ;
268
269
269
270
/**
270
271
* Gets the flow state that `flowstate` is transformed into.
@@ -275,7 +276,20 @@ abstract class BarrierFlowStateTransformer extends DataFlow::Node {
275
276
* transform(transform(x)) = transform(x)
276
277
* ```
277
278
*/
278
- abstract MaxValueState transform ( MaxValueState flowstate ) ;
279
+ MaxValueState transform ( MaxValueState state ) {
280
+ this .barrierFor ( state .getBitSize ( ) , state .getSinkBitSize ( ) ) and
281
+ result .getBitSize ( ) =
282
+ max ( int bitsize |
283
+ bitsize = validBitSize ( ) and
284
+ bitsize < state .getBitSize ( ) and
285
+ not this .barrierFor ( bitsize , state .getSinkBitSize ( ) )
286
+ ) and
287
+ (
288
+ result .getArchitectureBitSize ( ) = state .getArchitectureBitSize ( )
289
+ or
290
+ state .architectureBitSizeUnknown ( ) and result .architectureBitSizeUnknown ( )
291
+ )
292
+ }
279
293
}
280
294
281
295
private predicate upperBoundCheckGuard ( DataFlow:: Node g , Expr e , boolean branch ) {
@@ -372,31 +386,69 @@ class UpperBoundCheckGuard extends DataFlow::RelationalComparisonNode {
372
386
* for all flow states and would not transform any flow states, thus
373
387
* effectively blocking them.
374
388
*/
375
- class UpperBoundCheck extends BarrierFlowStateTransformer {
389
+ class UpperBoundCheck extends FlowStateTransformer {
376
390
UpperBoundCheckGuard g ;
377
391
378
392
UpperBoundCheck ( ) {
379
393
this = DataFlow:: BarrierGuard< upperBoundCheckGuard / 3 > :: getABarrierNodeForGuard ( g )
380
394
}
381
395
382
- override predicate barrierFor ( MaxValueState flowstate ) {
383
- g .isBoundFor ( flowstate . getBitSize ( ) , flowstate . getSinkBitSize ( ) )
396
+ override predicate barrierFor ( int bitSize , int architectureBitSize ) {
397
+ g .isBoundFor ( bitSize , architectureBitSize )
384
398
}
399
+ }
385
400
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 ( )
401
+ private predicate integerTypeBound ( IntegerType it , int bitSize , int architectureBitSize ) {
402
+ bitSize = validBitSize ( ) and
403
+ architectureBitSize = [ 32 , 64 ] and
404
+ exists ( int offset | if it instanceof SignedIntegerType then offset = 1 else offset = 0 |
405
+ if it instanceof IntType or it instanceof UintType
406
+ then bitSize >= architectureBitSize - offset
407
+ else bitSize >= it .getSize ( ) - offset
408
+ )
409
+ }
410
+
411
+ /**
412
+ * An expression which a type assertion guarantees will have a particular
413
+ * integer type.
414
+ *
415
+ * If this is a checked type expression then this value will only be used if
416
+ * the type assertion succeeded. If it is not checked then there will be a
417
+ * run-time panic if the type assertion fails, so we can assume it succeeded.
418
+ */
419
+ class TypeAssertionCheck extends DataFlow:: ExprNode , FlowStateTransformer {
420
+ IntegerType it ;
421
+
422
+ TypeAssertionCheck ( ) {
423
+ exists ( TypeAssertExpr tae |
424
+ this = DataFlow:: exprNode ( tae .getExpr ( ) ) and
425
+ it = tae .getTypeExpr ( ) .getType ( )
426
+ )
427
+ }
428
+
429
+ override predicate barrierFor ( int bitSize , int architectureBitSize ) {
430
+ integerTypeBound ( it , bitSize , architectureBitSize )
431
+ }
432
+ }
433
+
434
+ /**
435
+ * The implicit definition of a variable with integer type for a case clause of
436
+ * a type switch statement which declares a variable in its guard, which has
437
+ * effectively had a checked type assertion.
438
+ */
439
+ class TypeSwitchVarFlowStateTransformer extends DataFlow:: SsaNode , FlowStateTransformer {
440
+ IntegerType it ;
441
+
442
+ TypeSwitchVarFlowStateTransformer ( ) {
443
+ exists ( IR:: TypeSwitchImplicitVariableInstruction insn , LocalVariable lv | insn .writes ( lv , _) |
444
+ this .getSourceVariable ( ) = lv and
445
+ it = lv .getType ( )
398
446
)
399
447
}
448
+
449
+ override predicate barrierFor ( int bitSize , int architectureBitSize ) {
450
+ integerTypeBound ( it , bitSize , architectureBitSize )
451
+ }
400
452
}
401
453
402
454
/**
@@ -497,7 +549,10 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
497
549
498
550
predicate isBarrier ( DataFlow:: Node node , FlowState state ) {
499
551
// Safely guarded by a barrier guard.
500
- exists ( BarrierFlowStateTransformer bfst | node = bfst and bfst .barrierFor ( state ) )
552
+ exists ( FlowStateTransformer fst |
553
+ node = fst and
554
+ fst .barrierFor ( state .getBitSize ( ) , state .getSinkBitSize ( ) )
555
+ )
501
556
or
502
557
// When there is a flow from a source to a sink, do not allow the flow to
503
558
// continue to a further sink.
@@ -507,8 +562,8 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
507
562
predicate isAdditionalFlowStep (
508
563
DataFlow:: Node node1 , FlowState state1 , DataFlow:: Node node2 , FlowState state2
509
564
) {
510
- // Create additional flow steps for `BarrierFlowStateTransformer `s
511
- state2 = node2 .( BarrierFlowStateTransformer ) .transform ( state1 ) and
565
+ // Create additional flow steps for `FlowStateTransformer `s
566
+ state2 = node2 .( FlowStateTransformer ) .transform ( state1 ) and
512
567
DataFlow:: simpleLocalFlowStep ( node1 , node2 , _)
513
568
}
514
569
}
0 commit comments