Feature #7253
openShrink verifier (CPAchecker) logs intellectually
0%
Description
Verification reports for more or less big tasks are quite big (>700Mb for just one rule specification), most likely, because of logs of various components.
Thus several options for optimizations logs uploading are required in Bridge.
Here are a few potential options:
1. Upload only N last lines instead of the whole log. Usually the reason of unsuccessful termination is close to the end of log. For example, in CPAchecker we could limit log to average size of stats section (N=~200), which should include verdict and reason of termination.
2. Filter log by predefined tags. For example, we could remove from log every line, which starts with "DEBUG" or "Dead code detected:" in CPAchecker.
3. Analyse log and upload the reason of its termination. If the component was terminated successfully, we could upload the empty log. If it is possible to determine one of predefined reasons (time limit, assertion, etc.), we could upload the reason instead of the whole log (Klever already supports this partly). Thus we will upload the whole log only in case of unsuccessful termination and unknown reason of termination.
Updated by Evgeny Novikov over 8 years ago
- Subject changed from Uploading optimizations in Bridge to Shrink verifier (CPAchecker) logs intellectually
- Assignee set to Evgeny Novikov
- Priority changed from Normal to High
- One or more setting at the job start decision page.
- Extending verification tasks (this can be done directly by Bridge) since log files should be shrinked at the Task Worker side. Otherwise they will be include into verification task decisions and uploaded to Bridge.
- Shrinking log files in Task Worker (just for CPAchecker).