@@ -37,7 +37,6 @@ Stmt getPreviousStmt(Stmt s) {
3737 */
3838predicate firstUnreachableStmt ( Stmt s ) {
3939 not isReachable ( s ) and
40- not s instanceof EmptyStmt and
4140 (
4241 // a statement whose preceding statement in the same list is reachable
4342 isReachable ( getPreviousStmt ( s ) )
@@ -47,6 +46,16 @@ predicate firstUnreachableStmt(Stmt s) {
4746 )
4847}
4948
49+ /** Holds if `s` is in a run of unreachable statements following a constant condition. */
50+ predicate isInUnreachableRunAfterConstantCondition ( Stmt s ) {
51+ not isReachable ( s ) and
52+ (
53+ exists ( getPreviousStmt ( s ) .( IfStmt ) .getCondition ( ) .getBoolValue ( ) )
54+ or
55+ isInUnreachableRunAfterConstantCondition ( getPreviousStmt ( s ) )
56+ )
57+ }
58+
5059/**
5160 * Matches if `retval` is a constant or a struct composed wholly of constants.
5261 */
@@ -78,6 +87,8 @@ predicate isAllowedReturnValue(Expr retval) {
7887 * Matches if `s` is an allowed unreachable statement.
7988 */
8089predicate allowlist ( Stmt s ) {
90+ s instanceof EmptyStmt
91+ or
8192 // `panic("unreachable")` and similar
8293 exists ( CallExpr ce | ce = s .( ExprStmt ) .getExpr ( ) or ce = s .( ReturnStmt ) .getExpr ( ) |
8394 ce .getTarget ( ) .mustPanic ( ) or ce .getCalleeName ( ) .toLowerCase ( ) = "error"
@@ -87,14 +98,28 @@ predicate allowlist(Stmt s) {
8798 exists ( ReturnStmt ret | ret = s |
8899 forall ( Expr retval | retval = ret .getAnExpr ( ) | isAllowedReturnValue ( retval ) )
89100 )
90- or
91- // statements deliberately made unreachable by a constant condition, such as the code
92- // following `if true { return }`
93- exists ( getPreviousStmt ( s ) .( IfStmt ) .getCondition ( ) .getBoolValue ( ) )
101+ }
102+
103+ Stmt firstNonAllowlisted ( Stmt s ) {
104+ not isReachable ( s ) and
105+ (
106+ not allowlist ( s ) and result = s
107+ or
108+ allowlist ( s ) and
109+ exists ( Stmt next | getPreviousStmt ( next ) = s | result = firstNonAllowlisted ( next ) )
110+ )
111+ }
112+
113+ /** Holds if `s` is the first non-allowlisted statement in a run of unreachable statements. */
114+ predicate firstNonAllowlistedUnreachableStmt ( Stmt s ) {
115+ exists ( Stmt unreachable |
116+ firstUnreachableStmt ( unreachable ) and
117+ s = firstNonAllowlisted ( unreachable )
118+ )
94119}
95120
96121from Stmt s
97122where
98- firstUnreachableStmt ( s ) and
99- not allowlist ( s )
123+ firstNonAllowlistedUnreachableStmt ( s ) and
124+ not isInUnreachableRunAfterConstantCondition ( s )
100125select s , "This statement is unreachable."
0 commit comments