@@ -17,7 +17,7 @@ import semmle.code.cpp.controlflow.StackVariableReachability
1717/**
1818 * Holds if `node` overwrites `var` (assignment or declaration with initializer).
1919 */
20- predicate isDefOf ( ControlFlowNode node , StackVariable var ) {
20+ predicate isDefOf ( ControlFlowNode node , Variable var ) {
2121 node = var .getAnAccess ( ) and node .( VariableAccess ) .isLValue ( )
2222 or
2323 node .( DeclStmt ) .getADeclaration ( ) = var and exists ( var .getInitializer ( ) )
@@ -31,7 +31,7 @@ predicate isDefOf(ControlFlowNode node, StackVariable var) {
3131pragma [ nomagic]
3232predicate isDecInComparison (
3333 PostfixDecrExpr dec , VariableAccess varAcc ,
34- ComparisonOperation cmp , StackVariable var
34+ ComparisonOperation cmp , Variable var
3535) {
3636 varAcc = var .getAnAccess ( ) and
3737 dec .getOperand ( ) = varAcc .getExplicitlyConverted ( ) and
@@ -46,14 +46,14 @@ predicate isDecInComparison(
4646 * (i.e., a use that could observe an overflowed value).
4747 */
4848pragma [ nomagic]
49- predicate isReadOf ( VariableAccess va , StackVariable var ) {
49+ predicate isReadOf ( VariableAccess va , Variable var ) {
5050 va = var .getAnAccess ( ) and
5151 not exists ( AssignExpr ae | ae .getLValue ( ) = va )
5252}
5353
5454/**
5555 * Basic-block-level reachability from a decrement comparison to a use
56- * of the same variable, blocked by any definition of the variable.
56+ * of the same stack variable, blocked by any definition of the variable.
5757 */
5858class DecOverflowReach extends StackVariableReachability {
5959 DecOverflowReach ( ) { this = "DecOverflowReach" }
@@ -71,15 +71,62 @@ class DecOverflowReach extends StackVariableReachability {
7171 }
7272}
7373
74+ /**
75+ * BB-level reachability for non-stack variables (globals, static locals).
76+ * Holds if `sink` is reachable from the entry of `bb` without crossing
77+ * a definition of `var`.
78+ */
79+ private predicate nonStackBBEntryReaches (
80+ BasicBlock bb , Variable var , ControlFlowNode sink
81+ ) {
82+ exists ( int n |
83+ sink = bb .getNode ( n ) and
84+ isReadOf ( sink , var ) and
85+ not exists ( int m | m < n | isDefOf ( bb .getNode ( m ) , var ) )
86+ )
87+ or
88+ not isDefOf ( bb .getNode ( _) , var ) and
89+ nonStackBBEntryReaches ( bb .getASuccessor ( ) , var , sink )
90+ }
91+
92+ /**
93+ * BB-level reachability from `source` to `sink` for non-stack variables,
94+ * without crossing a definition of `var`.
95+ */
96+ pragma [ nomagic]
97+ predicate nonStackReaches (
98+ ComparisonOperation source , Variable var , ControlFlowNode sink
99+ ) {
100+ not var instanceof StackVariable and
101+ exists ( BasicBlock bb , int i |
102+ bb .getNode ( i ) = source and
103+ not bb .isUnreachable ( )
104+ |
105+ exists ( int j |
106+ j > i and
107+ sink = bb .getNode ( j ) and
108+ isReadOf ( sink , var ) and
109+ not exists ( int k | k in [ i + 1 .. j - 1 ] | isDefOf ( bb .getNode ( k ) , var ) )
110+ )
111+ or
112+ not exists ( int k | k > i | isDefOf ( bb .getNode ( k ) , var ) ) and
113+ nonStackBBEntryReaches ( bb .getASuccessor ( ) , var , sink )
114+ )
115+ }
116+
74117from
75- SemanticStackVariable var , VariableAccess varAcc , PostfixDecrExpr dec ,
118+ Variable var , VariableAccess varAcc , PostfixDecrExpr dec ,
76119 VariableAccess varAccAfterOverflow , ComparisonOperation cmp
77120where
78121 isDecInComparison ( dec , varAcc , cmp , var ) and
79122 isReadOf ( varAccAfterOverflow , var ) and
80123 varAcc != varAccAfterOverflow and
81- // reachable without intervening overwrite (basic-block-level analysis)
82- any ( DecOverflowReach r ) .reaches ( cmp , var , varAccAfterOverflow ) and
124+ // reachable without intervening overwrite
125+ (
126+ any ( DecOverflowReach r ) .reaches ( cmp , var , varAccAfterOverflow )
127+ or
128+ nonStackReaches ( cmp , var , varAccAfterOverflow )
129+ ) and
83130 // exclude accesses that are part of the comparison expression itself
84131 not cmp .getAnOperand ( ) .getAChild * ( ) = varAccAfterOverflow and
85132 // var-- > 0 (0 < var--) then only accesses in false branch matter
0 commit comments