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.