Skip to content

Commit 6337f5a

Browse files
geoffw0geoffw0
authored
Merge pull request #18586 from geoffw0/floatguards
C++: Test and (perhaps) fix an issue with guards on floating point comparisons.
2 parents 16634e6 + 67a746e commit 6337f5a

File tree

6 files changed

+435
-9
lines changed

6 files changed

+435
-9
lines changed

‎cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll

+35-8
Original file line numberDiff line numberDiff line change
@@ -102,49 +102,76 @@ abstract private class GuardConditionImpl extends Expr {
102102
this.valueControls(controlled, any(BooleanValue bv | bv.getValue() = testIsTrue))
103103
}
104104

105-
/** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
105+
/**
106+
* Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this
107+
* expression evaluates to `testIsTrue`. Note that there's a 4-argument
108+
* ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
109+
*/
106110
pragma[inline]
107111
abstract predicate comparesLt(Expr left, Expr right, int k, boolean isLessThan, boolean testIsTrue);
108112

109113
/**
110114
* Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`.
111-
* If `isLessThan = false` then this implies `left >= right + k`.
115+
* If `isLessThan = false` then this implies `left >= right + k`. Note that there's a 4-argument
116+
* ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
112117
*/
113118
pragma[inline]
114119
abstract predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan);
115120

116121
/**
117122
* Holds if (determined by this guard) `e < k` evaluates to `isLessThan` if
118-
* this expression evaluates to `value`.
123+
* this expression evaluates to `value`. Note that there's a 4-argument
124+
* ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
119125
*/
120126
pragma[inline]
121127
abstract predicate comparesLt(Expr e, int k, boolean isLessThan, AbstractValue value);
122128

123129
/**
124130
* Holds if (determined by this guard) `e < k` must be `isLessThan` in `block`.
125-
* If `isLessThan = false` then this implies `e >= k`.
131+
* If `isLessThan = false` then this implies `e >= k`. Note that there's a 4-argument
132+
* ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
126133
*/
127134
pragma[inline]
128135
abstract predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan);
129136

130-
/** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
137+
/**
138+
* Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this
139+
* expression evaluates to `testIsTrue`. Note that there's a 4-argument ("unary") and a
140+
* 5-argument ("binary") version of `comparesEq` and they are not equivalent:
141+
* - the unary version is suitable for guards where there is no expression representing the
142+
* right-hand side, such as `if (x)`, and also works for equality with an integer constant
143+
* (such as `if (x == k)`).
144+
* - the binary version is the more general case for comparison of any expressions (not
145+
* necessarily integer).
146+
*/
131147
pragma[inline]
132148
abstract predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue);
133149

134150
/**
135151
* Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
136-
* If `areEqual = false` then this implies `left != right + k`.
152+
* If `areEqual = false` then this implies `left != right + k`. Note that there's a 4-argument
153+
* ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
137154
*/
138155
pragma[inline]
139156
abstract predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual);
140157

141-
/** Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression evaluates to `value`. */
158+
/**
159+
* Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression
160+
* evaluates to `value`. Note that there's a 4-argument ("unary") and a 5-argument ("binary")
161+
* version of `comparesEq` and they are not equivalent:
162+
* - the unary version is suitable for guards where there is no expression representing the
163+
* right-hand side, such as `if (x)`, and also works for equality with an integer constant
164+
* (such as `if (x == k)`).
165+
* - the binary version is the more general case for comparison of any expressions (not
166+
* necessarily integer).
167+
*/
142168
pragma[inline]
143169
abstract predicate comparesEq(Expr e, int k, boolean areEqual, AbstractValue value);
144170

145171
/**
146172
* Holds if (determined by this guard) `e == k` must be `areEqual` in `block`.
147-
* If `areEqual = false` then this implies `e != k`.
173+
* If `areEqual = false` then this implies `e != k`. Note that there's a 4-argument
174+
* ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
148175
*/
149176
pragma[inline]
150177
abstract predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual);

‎cpp/ql/test/library-tests/controlflow/guards/Guards.expected

+15
Original file line numberDiff line numberDiff line change
@@ -77,3 +77,18 @@
7777
| test.cpp:193:8:193:9 | b1 |
7878
| test.cpp:193:8:193:15 | ... \|\| ... |
7979
| test.cpp:193:14:193:15 | b2 |
80+
| test.cpp:211:9:211:15 | ... == ... |
81+
| test.cpp:214:9:214:17 | ... == ... |
82+
| test.cpp:217:9:217:15 | ... == ... |
83+
| test.cpp:220:9:220:14 | ... == ... |
84+
| test.cpp:223:9:223:16 | ... == ... |
85+
| test.cpp:226:9:226:14 | ... == ... |
86+
| test.cpp:229:9:229:14 | ... == ... |
87+
| test.cpp:232:9:232:18 | ... == ... |
88+
| test.cpp:235:9:235:17 | ... == ... |
89+
| test.cpp:238:9:238:17 | ... == ... |
90+
| test.cpp:241:9:241:17 | ... == ... |
91+
| test.cpp:241:9:241:30 | ... && ... |
92+
| test.cpp:241:9:241:43 | ... && ... |
93+
| test.cpp:241:22:241:30 | ... == ... |
94+
| test.cpp:241:35:241:43 | ... == ... |

‎cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected

+113
Original file line numberDiff line numberDiff line change
@@ -653,3 +653,116 @@
653653
| 206 | c != 0 when c is true |
654654
| 206 | c == 0 when ! ... is true |
655655
| 206 | c == 0 when c is false |
656+
| 211 | 0 != sc+0 when ... == ... is false |
657+
| 211 | 0 == sc+0 when ... == ... is true |
658+
| 211 | ... == ... != 0 when ... == ... is true |
659+
| 211 | ... == ... != 1 when ... == ... is false |
660+
| 211 | ... == ... == 0 when ... == ... is false |
661+
| 211 | ... == ... == 1 when ... == ... is true |
662+
| 211 | sc != 0 when ... == ... is false |
663+
| 211 | sc != 0+0 when ... == ... is false |
664+
| 211 | sc == 0 when ... == ... is true |
665+
| 211 | sc == 0+0 when ... == ... is true |
666+
| 214 | 0 != sc+0 when ... == ... is false |
667+
| 214 | 0 == sc+0 when ... == ... is true |
668+
| 214 | ... == ... != 0 when ... == ... is true |
669+
| 214 | ... == ... != 1 when ... == ... is false |
670+
| 214 | ... == ... == 0 when ... == ... is false |
671+
| 214 | ... == ... == 1 when ... == ... is true |
672+
| 214 | sc != 0 when ... == ... is false |
673+
| 214 | sc != 0+0 when ... == ... is false |
674+
| 214 | sc == 0 when ... == ... is true |
675+
| 214 | sc == 0+0 when ... == ... is true |
676+
| 217 | 0 != ul+0 when ... == ... is false |
677+
| 217 | 0 == ul+0 when ... == ... is true |
678+
| 217 | ... == ... != 0 when ... == ... is true |
679+
| 217 | ... == ... != 1 when ... == ... is false |
680+
| 217 | ... == ... == 0 when ... == ... is false |
681+
| 217 | ... == ... == 1 when ... == ... is true |
682+
| 217 | ul != 0 when ... == ... is false |
683+
| 217 | ul != 0+0 when ... == ... is false |
684+
| 217 | ul == 0 when ... == ... is true |
685+
| 217 | ul == 0+0 when ... == ... is true |
686+
| 220 | 0 != f+0 when ... == ... is false |
687+
| 220 | 0 == f+0 when ... == ... is true |
688+
| 220 | ... == ... != 0 when ... == ... is true |
689+
| 220 | ... == ... != 1 when ... == ... is false |
690+
| 220 | ... == ... == 0 when ... == ... is false |
691+
| 220 | ... == ... == 1 when ... == ... is true |
692+
| 220 | f != 0+0 when ... == ... is false |
693+
| 220 | f == 0+0 when ... == ... is true |
694+
| 223 | 0.0 != f+0 when ... == ... is false |
695+
| 223 | 0.0 == f+0 when ... == ... is true |
696+
| 223 | ... == ... != 0 when ... == ... is true |
697+
| 223 | ... == ... != 1 when ... == ... is false |
698+
| 223 | ... == ... == 0 when ... == ... is false |
699+
| 223 | ... == ... == 1 when ... == ... is true |
700+
| 223 | f != 0.0+0 when ... == ... is false |
701+
| 223 | f == 0.0+0 when ... == ... is true |
702+
| 226 | 0 != d+0 when ... == ... is false |
703+
| 226 | 0 == d+0 when ... == ... is true |
704+
| 226 | ... == ... != 0 when ... == ... is true |
705+
| 226 | ... == ... != 1 when ... == ... is false |
706+
| 226 | ... == ... == 0 when ... == ... is false |
707+
| 226 | ... == ... == 1 when ... == ... is true |
708+
| 226 | d != 0+0 when ... == ... is false |
709+
| 226 | d == 0+0 when ... == ... is true |
710+
| 229 | 0 != b+0 when ... == ... is false |
711+
| 229 | 0 == b+0 when ... == ... is true |
712+
| 229 | ... == ... != 0 when ... == ... is true |
713+
| 229 | ... == ... != 1 when ... == ... is false |
714+
| 229 | ... == ... == 0 when ... == ... is false |
715+
| 229 | ... == ... == 1 when ... == ... is true |
716+
| 229 | b != 0 when ... == ... is false |
717+
| 229 | b != 0+0 when ... == ... is false |
718+
| 229 | b == 0 when ... == ... is true |
719+
| 229 | b == 0+0 when ... == ... is true |
720+
| 232 | 0 != b+0 when ... == ... is false |
721+
| 232 | 0 == b+0 when ... == ... is true |
722+
| 232 | ... == ... != 0 when ... == ... is true |
723+
| 232 | ... == ... != 1 when ... == ... is false |
724+
| 232 | ... == ... == 0 when ... == ... is false |
725+
| 232 | ... == ... == 1 when ... == ... is true |
726+
| 232 | b != 0 when ... == ... is false |
727+
| 232 | b != 0+0 when ... == ... is false |
728+
| 232 | b == 0 when ... == ... is true |
729+
| 232 | b == 0+0 when ... == ... is true |
730+
| 235 | 0 != i+0 when ... == ... is false |
731+
| 235 | 0 == i+0 when ... == ... is true |
732+
| 235 | ... == ... != 0 when ... == ... is true |
733+
| 235 | ... == ... != 1 when ... == ... is false |
734+
| 235 | ... == ... == 0 when ... == ... is false |
735+
| 235 | ... == ... == 1 when ... == ... is true |
736+
| 235 | i != 0 when ... == ... is false |
737+
| 235 | i != 0+0 when ... == ... is false |
738+
| 235 | i == 0 when ... == ... is true |
739+
| 235 | i == 0+0 when ... == ... is true |
740+
| 238 | 0 != f+0 when ... == ... is false |
741+
| 238 | 0 == f+0 when ... == ... is true |
742+
| 238 | ... == ... != 0 when ... == ... is true |
743+
| 238 | ... == ... != 1 when ... == ... is false |
744+
| 238 | ... == ... == 0 when ... == ... is false |
745+
| 238 | ... == ... == 1 when ... == ... is true |
746+
| 238 | f != 0+0 when ... == ... is false |
747+
| 238 | f == 0+0 when ... == ... is true |
748+
| 241 | 0 != f+0 when ... == ... is false |
749+
| 241 | 0 != i+0 when ... == ... is false |
750+
| 241 | 0 == f+0 when ... && ... is true |
751+
| 241 | 0 == f+0 when ... == ... is true |
752+
| 241 | 0 == i+0 when ... && ... is true |
753+
| 241 | 0 == i+0 when ... == ... is true |
754+
| 241 | ... == ... != 0 when ... && ... is true |
755+
| 241 | ... == ... != 0 when ... == ... is true |
756+
| 241 | ... == ... != 1 when ... == ... is false |
757+
| 241 | ... == ... == 0 when ... == ... is false |
758+
| 241 | ... == ... == 1 when ... && ... is true |
759+
| 241 | ... == ... == 1 when ... == ... is true |
760+
| 241 | f != 0+0 when ... == ... is false |
761+
| 241 | f == 0+0 when ... && ... is true |
762+
| 241 | f == 0+0 when ... == ... is true |
763+
| 241 | i != 0 when ... == ... is false |
764+
| 241 | i != 0+0 when ... == ... is false |
765+
| 241 | i == 0 when ... && ... is true |
766+
| 241 | i == 0 when ... == ... is true |
767+
| 241 | i == 0+0 when ... && ... is true |
768+
| 241 | i == 0+0 when ... == ... is true |

‎cpp/ql/test/library-tests/controlflow/guards/GuardsControl.expected

+18
Original file line numberDiff line numberDiff line change
@@ -146,3 +146,21 @@
146146
| test.cpp:193:8:193:15 | ... \|\| ... | false | 193 | 196 |
147147
| test.cpp:193:8:193:15 | ... \|\| ... | true | 197 | 199 |
148148
| test.cpp:193:14:193:15 | b2 | false | 192 | 193 |
149+
| test.cpp:211:9:211:15 | ... == ... | true | 211 | 212 |
150+
| test.cpp:214:9:214:17 | ... == ... | true | 214 | 215 |
151+
| test.cpp:217:9:217:15 | ... == ... | true | 217 | 218 |
152+
| test.cpp:220:9:220:14 | ... == ... | true | 220 | 221 |
153+
| test.cpp:223:9:223:16 | ... == ... | true | 223 | 224 |
154+
| test.cpp:226:9:226:14 | ... == ... | true | 226 | 227 |
155+
| test.cpp:229:9:229:14 | ... == ... | true | 229 | 230 |
156+
| test.cpp:232:9:232:18 | ... == ... | true | 232 | 233 |
157+
| test.cpp:235:9:235:17 | ... == ... | true | 235 | 236 |
158+
| test.cpp:238:9:238:17 | ... == ... | true | 238 | 239 |
159+
| test.cpp:241:9:241:17 | ... == ... | true | 241 | 241 |
160+
| test.cpp:241:9:241:17 | ... == ... | true | 241 | 242 |
161+
| test.cpp:241:9:241:30 | ... && ... | true | 241 | 241 |
162+
| test.cpp:241:9:241:30 | ... && ... | true | 241 | 242 |
163+
| test.cpp:241:9:241:43 | ... && ... | true | 241 | 242 |
164+
| test.cpp:241:22:241:30 | ... == ... | true | 241 | 241 |
165+
| test.cpp:241:22:241:30 | ... == ... | true | 241 | 242 |
166+
| test.cpp:241:35:241:43 | ... == ... | true | 241 | 242 |

0 commit comments

Comments
 (0)