Big performance regression of cbmc --cover in 6.0.1

[rod-chapman]

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]

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]

If you happen to have the time to do so, I would appreciate an evaluation of #8363 to see whether it changes the performance characteristics.

[rod-chapman]

I'll have a go...

[rod-chapman]

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]

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]

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]

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