Klever

I have done some necessary first steps of the refactoring to be able to integrate another tool but still there are many things to be done in this directon to make code tidy and clear for understanding. The major issues:

• Distinguish private methods (__mymethod), private inheritable methods (_mymethod), public methods (mymethod)
• Even if init function is not used there should be a function with list of attributes introduced by the strategy. Like methods all attributes should be distinguished concerning privateness.
• Implement clear algorithms for strategies with clear set of methods that can be implemented by another strategies derived from common ones. If it is necessary to introduce an hierarchy of strategies than should be able to understand where a general algorithm of a strategy is implemented and which steps are overrode or implemented differently. Currently functionality is very distributed and one cannot observe particular steps of any strategy because each contain just set of methods and its really hard to understand who calls them because there are called from many different places.
• Submitting tasks and getting results from Bridge and work with the other reports should be extracted into separate libraries inside VTG.
• It is forbidden to use attributes or methods in abstract strategies if there are introduced or logically belong to strategies which are inherited from this one. I removed all .mea, .mav and the other attributes from common strategies, but inside CPAchecker strategies (for example separated) there are a lot of inaccurate code left.

I suggest to remove all poorly established code from master and just support clear things that operate properly and reasonably. The only bad thing is that this will simplify components so that they will not allow to extend them even in the way that is available now. Perhaps this isn't very bad since eventually we can decide to give up experiments with multi-aspect verification and all its variants, for instance, if a more simpler, efficient and strong approach will be suggested instead.

After fixing of #7617 this issue will be relevant just for the specified experimental branch. Definitely it should be implemented there if we will want to merge this branch to master one day. Nevertheless I am absolutely not sure that we will decide this positively, so I don't see much sense to waste any resources on it while we always have issues of much more importance.

It is a part of 7799.

This issue likely will become irrelevant after refactoring.

This considerable Core refactoring is always completed and it would be better to have it in master ASAP while Klever 1.0 will be devoted to great conceptual improvements.

Implemented in the core-refactoring branch.

Major refactoring is almost finished. There are a couple of problems left and some minor introduced but it is better to deal with them separately. The refactoring included scaling parallel tasks generation, verifier options separation, templates for setting heap and limits in the option configuration file, support of the UltimateAutomizer verifier, deletion of verification tasks files during the progress and deletion them from the server, reuse of EMG and SA plugins data to avoid extra calls of CIF and speed up tasks generation, separation of tasks processing into additional components and many other helpful improvements. So I think that it is time to merge this as it is merged with the latest master branch and it becomes each next time more difficult.

At the moment common attributes as well as verification objects aren't reported for unsafe/safe/unknown reports that is absolutely crucial for creating corresponding marks. The former should be likely reported for VTGVRP while the latter for RP.

Update CPAchecker SMG up to version smg_witness_for_ldv:25566 - this was done in master about month ago.

Also I suppose to at last introduce one more component level between VTG (former AVTG) and its plugins. Otherwise plugin reports for various verification objects and rule specifications are intermixed. This issue existed before this refactoring as well.

Done all that you have requested in messages above. Check the new version, please.

A bug was introduced in this branch. At the moment failures of verification tasks generation plugins aren't reflected in resulting testing and validation tables.

All other mentioned below issues were fixed.

Yep, it works now.

1. If something wrong is with verifiers, e.g. I terminated them with a signal, then corresponding unknown reports are not children of verification reports - they are children of RP reports. This breaks preset unknown mark associations because of another component name.
2. I suggest that a meta component VTGVRP is redundant. Initially I thought to introduce it to unite working directories of Verification Tasks Generator and Verification Results Processor which are very similar because of they start with corresponding verification objects and rule specifications. But that wasn't done and I'm not sure that we will do it ever.
3. Both verification reports and their archives are now placed into working directories with ugly names. I suppose to use for them exactly the same names as were used before (some minor improvements are welcome) but create symlinks at corresponding paths to actual report and archive contents which is located in a dedicated directory now protected from removing before report uploading.

Other notes I mentioned directly in corresponding issues (#7803, #7924). For other related issues I didn't find any bugs. But I didn't play much with, say, verifier parameters and with integration of new static verification tools. Anyway at last we are moving forward in this direction.

If something wrong is with verifiers, ...

Done.

I suggest that a meta component VTGVRP is redundant.

I prefer to keep it as is because there are a lot of common shared data between VTG and VRP such as queues and directories. It is better to create the queues in VTGVRP and show that the components reuse dirs because they do their job as siblings of the one component.

Both verification reports and their archives are now placed into working directories with ugly names

Names contain the same data as previously but an identifier, so names are not completely useless at least comparing with the recent situation. The reason for the identifier is that in the same working directories happen reports with ununique names because of running components in the same dirs. I can try to remove identifiers for symlinks in components dirs but I cannot guarantee that it will work and it will require quite a comprehensive testing to check because some time ago it did not work. Moreover, reports are technical files intended for developers mostly and there are a lot of other important work to do other than complaining about ugly names of temporary files.

Ilja Zakharov wrote:

I suggest that a meta component VTGVRP is redundant.

I prefer to keep it as is because there are a lot of common shared data between VTG and VRP such as queues and directories. It is better to create the queues in VTGVRP and show that the components reuse dirs because they do their job as siblings of the one component.

Queues between the top level components are shared by hooking a special function called before those components are launched. You can find an example at the beginning of core/core/lkbce/_init__.py_.
I don't see any directory reuse because of VTG and VRP seem to create working directories independently on each other. There is just one extra parent directory for VTGVRP. Note that source tree directories are also "shadowed" within working directories of LKBCE and LKVOG but you didn't put them into the VTGVRP working directory.
Indeed I think that it will be great from some point of view if we will put everything related into the corresponding working directories. For instance, put a verification object description within a directory corresponding to a module path and put everything related with rule specifications within corresponding subdirectories within that one. But let's do that cool feature one day later.
Thus, if you can get rid of a redundant component, please, do it!

Both verification reports and their archives are now placed into working directories with ugly names

Names contain the same data as previously but an identifier, so names are not completely useless at least comparing with the recent situation. The reason for the identifier is that in the same working directories happen reports with ununique names because of running components in the same dirs. I can try to remove identifiers for symlinks in components dirs but I cannot guarantee that it will work and it will require quite a comprehensive testing to check because some time ago it did not work. Moreover, reports are technical files intended for developers mostly and there are a lot of other important work to do other than complaining about ugly names of temporary files.

First of all names don't contain the same data. I can't distinguish, say, start and finish component reports since there is just a number of meaningless symbols and "report" in report names while before they were named like "start report" and "finish report".

After another day of refactoring of the 'refactoring' I solved both issues. Now there is no VTGVRP and any data reuse between VTG and VRP except queues. For reports in component directories I have introduced cool and awesome names. Enjoy, I hope I have not introduced any additional bugs but it is worth checking.

P.S. To merge collateral branches for other core-related features intended for v0.2 an additional merge of this branch can be required.

After fixing several more issues I eventually merged the branch containing numerous cool improvements in Core to master in aec48ac1.