@@ -258,13 +258,14 @@ private class MaxValueState extends TMaxValueState {
258258 * A node that blocks some flow states and transforms some others as they flow
259259 * through it.
260260 */
261- abstract class BarrierFlowStateTransformer extends DataFlow:: Node {
261+ abstract class FlowStateTransformer extends DataFlow:: Node {
262262 /**
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`.
264265 *
265266 * This includes flow states which are transformed into other flow states.
266267 */
267- abstract predicate barrierFor ( MaxValueState flowstate ) ;
268+ abstract predicate barrierFor ( int bitSize , int architectureBitSize ) ;
268269
269270 /**
270271 * Gets the flow state that `flowstate` is transformed into.
@@ -275,7 +276,20 @@ abstract class BarrierFlowStateTransformer extends DataFlow::Node {
275276 * transform(transform(x)) = transform(x)
276277 * ```
277278 */
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+ }
279293}
280294
281295private predicate upperBoundCheckGuard ( DataFlow:: Node g , Expr e , boolean branch ) {
@@ -372,31 +386,69 @@ class UpperBoundCheckGuard extends DataFlow::RelationalComparisonNode {
372386 * for all flow states and would not transform any flow states, thus
373387 * effectively blocking them.
374388 */
375- class UpperBoundCheck extends BarrierFlowStateTransformer {
389+ class UpperBoundCheck extends FlowStateTransformer {
376390 UpperBoundCheckGuard g ;
377391
378392 UpperBoundCheck ( ) {
379393 this = DataFlow:: BarrierGuard< upperBoundCheckGuard / 3 > :: getABarrierNodeForGuard ( g )
380394 }
381395
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 )
384398 }
399+ }
385400
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 ( )
398446 )
399447 }
448+
449+ override predicate barrierFor ( int bitSize , int architectureBitSize ) {
450+ integerTypeBound ( it , bitSize , architectureBitSize )
451+ }
400452}
401453
402454/**
@@ -497,7 +549,10 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
497549
498550 predicate isBarrier ( DataFlow:: Node node , FlowState state ) {
499551 // 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+ )
501556 or
502557 // When there is a flow from a source to a sink, do not allow the flow to
503558 // continue to a further sink.
@@ -507,8 +562,8 @@ private module ConversionWithoutBoundsCheckConfig implements DataFlow::StateConf
507562 predicate isAdditionalFlowStep (
508563 DataFlow:: Node node1 , FlowState state1 , DataFlow:: Node node2 , FlowState state2
509564 ) {
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
512567 DataFlow:: simpleLocalFlowStep ( node1 , node2 , _)
513568 }
514569}
0 commit comments