Commit d9951b7
authored
Optimize goto binary exporting in
Motivated by the finding that the
[`write_goto_binary_file`](https://github.com/model-checking/kani/blob/1b25a1853fab3262380e9baefdfeb929edd53fd1/cprover_bindings/src/irep/goto_binary_serde.rs#L97-L103)
function is responsible for around half of our compiler's codegen time,
this PR does a collection of low-hanging fruit optimizations for the way
we export goto files in the `cprover_bindings` crate.
This includes:
- Switching `IrepNumbering` caches to use the faster
[`FxHashMap`](https://nnethercote.github.io/2021/12/08/a-brutally-effective-hash-function-in-rust.html)
(as used in the rust compiler)
- Using `.entry().or_insert()` to initialize the irep cache
- This avoids having to hash separately for a `.get()` and `.insert()`
(as the compiler seemed to have not optimized them together)
- Making `IrepId` strings copy-on-write
- This avoids unnecessary string allocations by allowing us to construct
`InternedString`s directly from borrowed string literals when possible
Initial testing (on
[`perf/format`](https://github.com/model-checking/kani/blob/main/tests/perf/format/src/lib.rs)
&
[`perf/vec/vec`](https://github.com/model-checking/kani/blob/main/tests/perf/vec/vec/src/main.rs))
suggests that these changes make our compiler ~13% faster, but I'm also
working on comparing performance on the whole std project for the
future.
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.cprover_bindings (#4148)1 parent 5b6700e commit d9951b7
File tree
4 files changed
+95
-30
lines changed- cprover_bindings
- src/irep
4 files changed
+95
-30
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
190 | 190 | | |
191 | 191 | | |
192 | 192 | | |
| 193 | + | |
| 194 | + | |
| 195 | + | |
| 196 | + | |
| 197 | + | |
| 198 | + | |
193 | 199 | | |
194 | 200 | | |
195 | 201 | | |
| |||
406 | 412 | | |
407 | 413 | | |
408 | 414 | | |
| 415 | + | |
409 | 416 | | |
410 | 417 | | |
411 | 418 | | |
| |||
681 | 688 | | |
682 | 689 | | |
683 | 690 | | |
| 691 | + | |
| 692 | + | |
| 693 | + | |
| 694 | + | |
| 695 | + | |
| 696 | + | |
| 697 | + | |
| 698 | + | |
| 699 | + | |
684 | 700 | | |
685 | 701 | | |
686 | 702 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
20 | 20 | | |
21 | 21 | | |
22 | 22 | | |
| 23 | + | |
23 | 24 | | |
24 | 25 | | |
25 | 26 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
80 | 80 | | |
81 | 81 | | |
82 | 82 | | |
| 83 | + | |
| 84 | + | |
| 85 | + | |
83 | 86 | | |
84 | 87 | | |
85 | 88 | | |
| |||
199 | 202 | | |
200 | 203 | | |
201 | 204 | | |
| 205 | + | |
| 206 | + | |
| 207 | + | |
| 208 | + | |
| 209 | + | |
| 210 | + | |
| 211 | + | |
| 212 | + | |
| 213 | + | |
| 214 | + | |
| 215 | + | |
| 216 | + | |
| 217 | + | |
| 218 | + | |
| 219 | + | |
| 220 | + | |
| 221 | + | |
| 222 | + | |
| 223 | + | |
| 224 | + | |
202 | 225 | | |
| 226 | + | |
203 | 227 | | |
204 | 228 | | |
205 | 229 | | |
| |||
214 | 238 | | |
215 | 239 | | |
216 | 240 | | |
| 241 | + | |
217 | 242 | | |
218 | 243 | | |
219 | 244 | | |
220 | | - | |
| 245 | + | |
221 | 246 | | |
222 | | - | |
| 247 | + | |
223 | 248 | | |
224 | 249 | | |
225 | 250 | | |
| 251 | + | |
226 | 252 | | |
| 253 | + | |
| 254 | + | |
| 255 | + | |
| 256 | + | |
| 257 | + | |
| 258 | + | |
| 259 | + | |
| 260 | + | |
| 261 | + | |
| 262 | + | |
| 263 | + | |
| 264 | + | |
| 265 | + | |
227 | 266 | | |
228 | 267 | | |
229 | 268 | | |
| |||
248 | 287 | | |
249 | 288 | | |
250 | 289 | | |
251 | | - | |
| 290 | + | |
252 | 291 | | |
253 | 292 | | |
254 | 293 | | |
| |||
264 | 303 | | |
265 | 304 | | |
266 | 305 | | |
267 | | - | |
| 306 | + | |
268 | 307 | | |
269 | 308 | | |
270 | 309 | | |
271 | 310 | | |
272 | | - | |
273 | | - | |
274 | | - | |
275 | | - | |
276 | | - | |
277 | | - | |
278 | | - | |
279 | | - | |
280 | | - | |
| 311 | + | |
| 312 | + | |
| 313 | + | |
| 314 | + | |
| 315 | + | |
| 316 | + | |
| 317 | + | |
281 | 318 | | |
282 | 319 | | |
283 | 320 | | |
| |||
794 | 831 | | |
795 | 832 | | |
796 | 833 | | |
797 | | - | |
| 834 | + | |
798 | 835 | | |
799 | 836 | | |
800 | 837 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
8 | 8 | | |
9 | 9 | | |
10 | 10 | | |
11 | | - | |
| 11 | + | |
12 | 12 | | |
13 | 13 | | |
14 | 14 | | |
| |||
877 | 877 | | |
878 | 878 | | |
879 | 879 | | |
880 | | - | |
881 | | - | |
| 880 | + | |
| 881 | + | |
| 882 | + | |
| 883 | + | |
| 884 | + | |
| 885 | + | |
| 886 | + | |
| 887 | + | |
| 888 | + | |
| 889 | + | |
| 890 | + | |
| 891 | + | |
| 892 | + | |
| 893 | + | |
| 894 | + | |
| 895 | + | |
| 896 | + | |
| 897 | + | |
882 | 898 | | |
883 | | - | |
884 | | - | |
885 | | - | |
886 | | - | |
887 | | - | |
888 | | - | |
889 | | - | |
890 | | - | |
891 | | - | |
892 | | - | |
| 899 | + | |
| 900 | + | |
| 901 | + | |
| 902 | + | |
893 | 903 | | |
| 904 | + | |
894 | 905 | | |
895 | | - | |
| 906 | + | |
| 907 | + | |
896 | 908 | | |
897 | 909 | | |
898 | 910 | | |
| |||
1719 | 1731 | | |
1720 | 1732 | | |
1721 | 1733 | | |
1722 | | - | |
1723 | | - | |
| 1734 | + | |
1724 | 1735 | | |
1725 | 1736 | | |
1726 | 1737 | | |
| |||
0 commit comments