@@ -11,6 +11,19 @@ private predicate mayAddNullTerminatorHelper(Expr e, VariableAccess va, Expr e0)
11
11
)
12
12
}
13
13
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
+
14
27
/**
15
28
* Holds if the expression `e` may add a null terminator to the string in
16
29
* variable `v`.
@@ -30,14 +43,9 @@ predicate mayAddNullTerminator(Expr e, VariableAccess va) {
30
43
)
31
44
or
32
45
// Assignment to another stack variable
33
- exists ( Expr e0 , BasicBlock bb , int pos , BasicBlock bb0 , int pos0 |
46
+ exists ( Expr e0 |
34
47
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 )
41
49
)
42
50
or
43
51
// Assignment to non-stack variable
@@ -119,14 +127,9 @@ predicate variableMustBeNullTerminated(VariableAccess va) {
119
127
variableMustBeNullTerminated ( use ) and
120
128
// Simplified: check that `p` may not be null terminated on *any*
121
129
// 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 |
123
131
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 )
130
133
)
131
134
)
132
135
)
0 commit comments