diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
815 stars 258 forks source link

Big performance regression of cbmc --cover in 6.0.1 #8389

Open rod-chapman opened 1 month ago

rod-chapman commented 1 month ago

CBMC version: 6.0.1 Operating system: macOS Exact command line resulting in the issue: cbmc --flush --object-bits 8 --unwindset strlen.0:5,strncmp.0:5,__CPROVER_file_local_s2n_stuffer_pem_c_s2n_stuffer_pem_read_contents.11:11,s2n_stuffer_skip_to_char.0:11 --unwind 1 --malloc-may-fail --malloc-fail-null --cover location s2n_spkfph601.goto What behaviour did you expect: complete in 16 seconds What happened instead: completes in 2286 seconds

Details and artefacts to follow once Issue number is allocated.

rod-chapman commented 1 month ago

See artefacts here: https://github.com/rod-chapman/cbmc-examples/tree/main/issues/8389

Background: Running CBMC 6.0.1 (wavefront of 18th July), I am getting a huge performance drop on the proof of one function in s2n-tls.

See the artefacts in the directory linked above.

The command

cbmc --flush --object-bits 8 --unwindset strlen.0:5,strncmp.0:5,__CPROVER_file_local_s2n_stuffer_pem_c_s2n_stuffer_pem_read_contents.11:11,s2n_stuffer_skip_to_char.0:11 --unwind 1 --malloc-may-fail --malloc-fail-null --cover location s2n_spkfph601.goto

with CBMC 6.0.1 takes 2286 seconds (38 minutes) to run on my MacBook Pro.

With CBMC 5.95.1 (running on the 5.95.1 version of the goto file) it takes 16 seconds.

This performance degradation is sufficient to break s2n-tls's CI run.

The artefacts are: s2n_spkfph.goto - GOTO file generated by CBMC 5.95.1 and 6.0.1 respectively s2n_spkfph_std.goto - stdout and stderr files generated by running the above command with 5.95.1 and 6.0.1 show_functions.txt - results of running "goto-inspect --show-goto-functions" on the goto files above.

tautschnig commented 1 month ago

If you happen to have the time to do so, I would appreciate an evaluation of https://github.com/diffblue/cbmc/pull/8363 to see whether it changes the performance characteristics.

rod-chapman commented 1 month ago

I'll have a go...

rod-chapman commented 1 month ago

I added the GOTO file generated by your new branch here: https://github.com/rod-chapman/cbmc-examples/tree/main/issues/8389 Bottom line: performance still very slow...

rod-chapman commented 1 month ago

Results are in: 2292 seconds on your branch, so no better than 6.0.1, and still 140 times slower than 5.95.1

tautschnig commented 1 month ago

Adding --no-standard-checks makes all the difference and brings runtime back to what it used to be; without this option we have various newly-default-on checks (such as pointer checks) inserted as assumptions during coverage checking. I think we need to revisit this as some of those don't make a whole lot of sense as assumptions.

Until we have resolved this: you can add COVERFLAGS := --no-standard-checks when you are using the starter kit.

rod-chapman commented 1 month ago

OK... all proofs of s2n-tls now run on 7min 30secs using 8 cores on a MacBook Pro, so looking good!