CBMC/JBMC --cover: only store traces with --trace to avoid memory exhaustion #5714
Conversation
tautschnig
requested review from
chrisr-diffblue,
hannes-steffenhagen-diffblue,
kroening,
peterschrammel and
smowton
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #5714 +/- ##
===========================================
- Coverage 69.67% 69.66% -0.02%
===========================================
Files 1248 1248
Lines 100836 100854 +18
===========================================
Hits 70262 70262
- Misses 30574 30592 +18
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
There was a problem hiding this comment.
Good workaround in the meanwhile. Storing traces and inputs should be decoupled, though, I think.
Besides, I should probably revive the PR that enables trace output as traces are produced rather than storing them at all (but that's quite a UI change which needs to be phased in properly).
| @@ -1,6 +1,6 @@ | |||
| CORE | |||
| main.c | |||
| --xml-ui --cover branch | |||
| --xml-ui --cover branch --trace | |||
There was a problem hiding this comment.
Seems like this is broken somehow?
There was a problem hiding this comment.
Yes, it was broken as the code generating XML output is used for both trace and test-suite output. I have therefore changed the patch to introduce a new command-line option "show-test-suite."
There was a problem hiding this comment.
Given the performance numbers this sounds very much like the kind of thing we want and I am in favour of not storing things we don't need. But I am a little confused over the use-case for this. --cover creates a bunch of assertions for the relevant coverage metric and then solves for all of them. Then, orthogonally(? is this what @peterschrammel is suggesting?) we could output for each location:
A. reached / unreachable.
B. inputs that would cause the relevant path to be taken.
C. the execution trace that reaches each one.
So this is only fro case C? Are there users of this? Also, can't we output these as we compute them? I'm not sure I see why they need to be stored at all.
goto traces consume a lot of memory, and re-allocating them for each incremental addition of a goto trace does not seem to be a good approach. This is at the expense of more costly indexed access, which now requires iterator increments.
tautschnig
force-pushed
the
cover-trace
branch
from
65d381f to
0fe9312
Compare
|
@peterschrammel @martin-cs I'd appreciate you taking another look at this for I've made substantial changes over the version you previously reviewed/approved:
It may still be desirable to print test inputs as-you-go, but that's not something on my priority queue (as I don't care about those inputs values at the moment). |
A goto trace includes freshly constructed expressions, which thus lack sharing. This results in excessive memory use when storing multiple traces, as is done for coverage computation. On a particular benchmark, coverage computation previously ran out of memory at 768 GB. This same benchmark can now be run with just 80 GB of memory.
tautschnig
force-pushed
the
cover-trace
branch
from
0fe9312 to
a18c47d
Compare
tautschnig
force-pushed
the
cover-trace
branch
from
a18c47d to
b3025b1
Compare
Not everyone needs test inputs, especially when programs lack INPUT instructions anyway. Test inputs are found via goto traces, and computing those is expensive in both time and memory required. On one benchmark, not building goto traces reduced the overall time from 36000 seconds to 2800 seconds (a saving of 92%).
tautschnig
force-pushed
the
cover-trace
branch
from
b3025b1 to
87e8440
Compare
|
@tautschnig Apologies for the lag; first week of term. I'm guessing by the merge that you are happy with this. |
Not everyone needs test inputs, especially when programs lack INPUT
instructions anyway. This helped me avoid running out of memory on a
768GB system for a particular verification problem. The same problem can
now be run with just 75GB of memory.