@@ -11,6 +11,19 @@ private predicate mayAddNullTerminatorHelper(Expr e, VariableAccess va, Expr e0)
1111 )
1212}
1313
14+ bindingset [ n1, n2]
15+ predicate nodeBefore ( ControlFlowNode n1 , ControlFlowNode n2 ) {
16+ exists ( BasicBlock bb1 , int pos1 , BasicBlock bb2 , int pos2 |
17+ pragma [ only_bind_into ] ( bb1 ) .getNode ( pos1 ) = n1 and
18+ pragma [ only_bind_into ] ( bb2 ) .getNode ( pos2 ) = n2 and
19+ (
20+ bb1 = bb2 and pos1 < pos2
21+ or
22+ bb1 .getASuccessor + ( ) = bb2
23+ )
24+ )
25+ }
26+
1427/**
1528 * Holds if the expression `e` may add a null terminator to the string in
1629 * variable `v`.
@@ -30,14 +43,9 @@ predicate mayAddNullTerminator(Expr e, VariableAccess va) {
3043 )
3144 or
3245 // Assignment to another stack variable
33- exists ( Expr e0 , BasicBlock bb , int pos , BasicBlock bb0 , int pos0 |
46+ exists ( Expr e0 |
3447 mayAddNullTerminatorHelper ( pragma [ only_bind_into ] ( e ) , va , pragma [ only_bind_into ] ( e0 ) ) and
35- pragma [ only_bind_into ] ( bb ) .getNode ( pos ) = e and
36- pragma [ only_bind_into ] ( bb0 ) .getNode ( pos0 ) = e0
37- |
38- bb = bb0 and pos < pos0
39- or
40- bb .getASuccessor + ( ) = bb0
48+ nodeBefore ( e0 , e )
4149 )
4250 or
4351 // Assignment to non-stack variable
@@ -119,14 +127,9 @@ predicate variableMustBeNullTerminated(VariableAccess va) {
119127 variableMustBeNullTerminated ( use ) and
120128 // Simplified: check that `p` may not be null terminated on *any*
121129 // path to `use` (including the one found via `parameterUsePair`)
122- not exists ( Expr e , BasicBlock bb1 , int pos1 , BasicBlock bb2 , int pos2 |
130+ not exists ( Expr e |
123131 mayAddNullTerminator ( pragma [ only_bind_into ] ( e ) , p .getAnAccess ( ) ) and
124- pragma [ only_bind_into ] ( bb1 ) .getNode ( pos1 ) = e and
125- bb2 .getNode ( pos2 ) = use
126- |
127- bb1 = bb2 and pos1 < pos2
128- or
129- bb1 .getASuccessor + ( ) = bb2
132+ nodeBefore ( e , use )
130133 )
131134 )
132135 )
0 commit comments