https://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692018-12-12T14:00:30ZOpen-Source ProjectsKlever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=353982018-12-12T14:00:30ZVitaly Mordanmordan@ispras.ru
<ul><li><strong>Related to</strong> <i><a class="issue tracker-4 status-5 priority-6 priority-high2 closed" href="/issues/8704">Feature #8704</a>: Support processing of multiple error traces per one unsafe report</i> added</li></ul> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=353992018-12-12T14:17:32ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>New</i> to <i>Rejected</i></li></ul><p>There is not this issue, since you do can specify various attributes for different error traces within one report. Klever already does this - you can find that Klever does not report any attributes for error traces in reports explicitly. The trick is including Klever attributes within witnesses. Witnesses with data races started to use this trick a long ago, so, you can learn the format from them.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354002018-12-12T14:39:50ZPavel Andrianovandrianov@ispras.ru
<ul></ul><p>Some attributes can be related not to a witness, but to a whole launch. So, the feature is only not to clone the same "sources.zip", if it occurs several times.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354012018-12-12T14:42:58ZVitaly Mordanmordan@ispras.ru
<ul></ul><p>Now each unsafe node is tied to verification node (with resources, logs, etc.).<br />Unlike variable names in races, some attributes do not relate to witness at all.<br />Do you suggest to create a single node for all error trace to lose all that information and components hierarchy?<br />This is very bad suggestion.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354022018-12-12T14:45:41ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Pavel Andrianov wrote:</p>
<blockquote>
<p>Some attributes can be related not to a witness, but to a whole launch. So, the feature is only not to clone the same "sources.zip", if it occurs several times.</p>
</blockquote>
<p>If you need the same attributes for all underlying reports, you need to upload them within a parent report, most likely within verification reports.</p>
<p>As far as I understand, very old Bridge did detect file duplicates, but it was quite hard to do.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354032018-12-12T14:48:36ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Vitaly Mordan wrote:</p>
<blockquote>
<p>Now each unsafe node is tied to verification node (with resources, logs, etc.).<br />Unlike variable names in races, some attributes do not relate to witness at all.<br />Do you suggest to create a single node for all error trace to lose all that information and components hierarchy?<br />This is very bad suggestion.</p>
</blockquote>
<p>What is an unsafe node? What is a verification node?</p>
<p>If attributes are not related with witnesses, you should not upload them with help of unsafe reports.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354042018-12-12T14:53:20ZPavel Andrianovandrianov@ispras.ru
<ul></ul><blockquote>
<p>If you need the same attributes for all underlying reports, you need to upload them within a parent report, most likely within verification reports.</p>
</blockquote>
<p>Yes, but in this case we have to create several unsafe reports with the same "source.zip", which will be cloned by bridge.</p>
<blockquote>
<p>As far as I understand, very old Bridge did detect file duplicates, but it was quite hard to do.</p>
</blockquote>
<p>We just request to resolve file names, so if "source.zip" is contained in several unsafe reports, it should be cloned, while uploading.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354052018-12-12T14:54:32ZPavel Andrianovandrianov@ispras.ru
<ul></ul><blockquote>
<p>What is an unsafe node? What is a verification node?</p>
</blockquote>
<p>This is unsafe report and verification report.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354072018-12-12T15:03:25ZVitaly Mordanmordan@ispras.ru
<ul></ul><p>For example, we have the following hierarchy of nodes in report:<br />-root<br />--Component1<br />--Component2<br />---CPAchecker_1<br />----unsafe (sources=sources.zip)<br />----unknown<br />---CPAchecker_N<br />----unsafe (sources=sources.zip)<br />----unknown</p>
<blockquote>
<p>If you need the same attributes for all underlying reports, you need to upload them within a parent report, most likely within verification reports.</p>
</blockquote>
<p>Here we need attributes, resources, logs and such of verification report (CPAchecker_i) for each leaf, therefore I will not merge them.<br />At the same time, each unsafe report have a link to sources.zip, which should not be duplicated on uploading.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354082018-12-12T15:04:30ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Pavel Andrianov wrote:</p>
<blockquote><blockquote>
<p>If you need the same attributes for all underlying reports, you need to upload them within a parent report, most likely within verification reports.</p>
</blockquote>
<p>Yes, but in this case we have to create several unsafe reports with the same "source.zip", which will be cloned by bridge.</p>
</blockquote>
<p>Can't you create an intermediate reports of another type? E.g.:</p>
<pre>
verification report with common attributes:
unsafe report with common sources and one or more error traces with specific attributes
</pre>
<p>If you can't, Bridge should support this rather than the strange thing suggested below.</p>
<blockquote><blockquote>
<p>As far as I understand, very old Bridge did detect file duplicates, but it was quite hard to do.</p>
</blockquote>
<p>We just request to resolve file names, so if "source.zip" is contained in several unsafe reports, it should be cloned, while uploading.</p>
</blockquote>
<p>But there can be files with the same names but various contents. So, it seems you suggest a workaround rather than to do things in the right way.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354092018-12-12T15:17:11ZVitaly Mordanmordan@ispras.ru
<ul></ul><p>Evgeny Novikov wrote:</p>
<blockquote>
<p>But there can be files with the same names but various contents. So, it seems you suggest a workaround rather than to do things in the right way.</p>
</blockquote>
<p>This is not possible, since each archive contains absolute paths to the source files.<br />If you need different sources, you can create several archives and add links to them:<br />-unsafe (sources=sources_1.zip, trace=t_1.zip)<br />-unsafe (sources=sources_1.zip, trace=t_2.zip)<br />-unsafe (sources=sources_2.zip, trace=t_3.zip)<br />Again, in this case you will need 2 archives with sources (not 3).</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354102018-12-12T15:20:40ZPavel Andrianovandrianov@ispras.ru
<ul></ul><blockquote>
<p>Can't you create an intermediate reports of another type?</p>
</blockquote>
<p>We do it already (see example from Vitaly), but it does not help for the problem: anyway we need to create several different unsafe reports with the same "sources.zip".</p>
<blockquote>
<p>But there can be files with the same names but various contents.</p>
</blockquote>
<p>I hardly can imagine this. How can an archive contain two different files with the same name?</p>
<p>I can suggest another idea, if you liked it more. Could the Bridge get sources not only from the unsafe report, but also from parent ones. So, if the sources are specified for a common parent, it is considered as it is specified for all child reports. It is important, that in this case the sources are not duplicated for all children.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354122018-12-13T07:30:08ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Rejected</i> to <i>Open</i></li><li><strong>Assignee</strong> set to <i>Vladimir Gratinskiy</i></li><li><strong>Priority</strong> changed from <i>Normal</i> to <i>Urgent</i></li><li><strong>Target version</strong> set to <i>3.0</i></li></ul><p>Pavel Andrianov wrote:</p>
<blockquote><blockquote>
<p>Can't you create an intermediate reports of another type?</p>
</blockquote>
<p>We do it already (see example from Vitaly), but it does not help for the problem: anyway we need to create several different unsafe reports with the same "sources.zip".</p>
</blockquote>
<p>Now I catch the issue at last. First of all, I am not sure that you prepare reports in the proper way. As far as I rememember there can be the only verification report for the same parent (Vladimir, am I right?). If you violate this assumption, you should expect various issues in Bridge, e.g. comparison of verification results will not work. I am wondering, why Bridge does not reject your reports - this should be fixed.</p>
<p>But when you will upload reports properly, this will not help to solve the issue. Below you suggested a nice way to fix it.</p>
<blockquote><blockquote>
<p>But there can be files with the same names but various contents.</p>
</blockquote>
<p>I hardly can imagine this. How can an archive contain two different files with the same name?</p>
<p>I can suggest another idea, if you liked it more. Could the Bridge get sources not only from the unsafe report, but also from parent ones. So, if the sources are specified for a common parent, it is considered as it is specified for all child reports. It is important, that in this case the sources are not duplicated for all children.</p>
</blockquote>
<p>After all there should be something like:<br /><pre>
Core report
Component1 report
Component2 report
sources.zip # This is a new feature to be supported by Bridge. It should use this archive for all error traces in subtree below.
Component2-1 report
Verification1 report
Attributes1
Log1
Resources1
Unsafe1 report
Component2-2 report
Verification2 report
Attributes2
Log2
Resources2
Unsafe2 report
Unknown2 report
</pre></p>
<p>Please, not that for comparison Bridge will consider unique tuples of values of cumulative verification report attributes marked to be used for comparison. For instance, if "Verification1 report" has attribute A with value A1 and one Unsafe report, and "Verification2 report" has attribute A with value A2, one Unsafe report and one Unknown report, and attribute A is marked to be used for comparison, then Bridge will compare these verification results with other ones by constructing tuples (A1) and (A2) for which total verdicts will be "Found all unsafes" and "Found not all unsafes". If you will report verification results using another approach to have some other features, you will lose an ability to compare verification results and perhaps something else.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354142018-12-13T08:16:19ZPavel Andrianovandrianov@ispras.ru
<ul></ul><blockquote>
<p>As far as I rememember there can be the only verification report for the same parent (Vladimir, am I right?)</p>
</blockquote>
<p>Neither specification format, nor implementation has such restriction. Anyway, a single component (Verifier) can be launched several times in a one launch, so, it produces several verification reports. Thus I do not consider the restriction to be relevant.</p>
<blockquote>
<p>After all there should be something like:</p>
</blockquote>
<p>I am not against the new features as in your example. I would just say that add several lines to check the name and not to clone it is much more easier than to implement such large feature. For this particular problem it looks like "To use a sledge-hammer to crack a nut."</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354162018-12-13T08:44:39ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Open</i> to <i>Feedback</i></li></ul><p>Pavel Andrianov wrote:</p>
<blockquote><blockquote>
<p>As far as I rememember there can be the only verification report for the same parent (Vladimir, am I right?)</p>
</blockquote>
<p>Neither specification format, nor implementation has such restriction. Anyway, a single component (Verifier) can be launched several times in a one launch, so, it produces several verification reports. Thus I do not consider the restriction to be relevant.</p>
</blockquote>
<p>Let's wait an answer from Vladimir. For me it seems to be a bug in Bridge since it does not make corresponding jobs corrupted due to incorrect reports. And later different operations may fail unexpectedly, in particular after updating Bridge.</p>
<p>Klever was never intended for things you are talking about. Of course, you can do very many various ones, e.g. launch various verifiers using conditions and maybe loops, use different configurations and so on, but then you have to prepare the only verification report with all verification results as its children. According to this it looks like the original issue is not relevant for Klever at all.</p>
<p>BTW, if you want to describe some useful information about your complex verification strategy, you can use advanced features of attributes, in particular data attributes, and upload many files rather than one. If you dislike this approach, do not expect that you will be able to use Bridge safely.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354172018-12-13T09:06:26ZPavel Andrianovandrianov@ispras.ru
<ul></ul><blockquote>
<p>then you have to prepare the only verification report with all verification results as its children.</p>
</blockquote>
<p>Then I have no possibility to describe all verifiers I used, as I have to prepare only one verification report per all launches. For example, one of the launch failed with exception, the other found several unsafes and finish with timeout and the last one suddenly proved true. Now there is a restriction, that a safe verdict can not be combined with unsafe or unknown, which is reasonable. Also, there are different resources, logs and so on. It is not correct to put all this data into different attributes of unsafe reports. Thus I still consider the restriction 'only one verification report' as irrelevant.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354182018-12-13T09:39:01ZVladimir Gratinskiygratinskiy@ispras.ru
<ul></ul><p>Evgeny Novikov wrote:</p>
<blockquote>
<p>As far as I rememember there can be the only verification report for the same parent (Vladimir, am I right?).</p>
</blockquote>
<p>There is no such restriction.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354232018-12-13T10:22:48ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Vladimir Gratinskiy wrote:</p>
<blockquote>
<p>Evgeny Novikov wrote:</p>
<blockquote>
<p>As far as I rememember there can be the only verification report for the same parent (Vladimir, am I right?).</p>
</blockquote>
<p>There is no such restriction.</p>
</blockquote>
<p>Okay. Does Bridge compare verification results on the basis of verification reports? That's it calculates a total verdict for a given verification report and all its children?</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354242018-12-13T10:26:57ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Pavel Andrianov wrote:</p>
<blockquote><blockquote>
<p>then you have to prepare the only verification report with all verification results as its children.</p>
</blockquote>
<p>Then I have no possibility to describe all verifiers I used, as I have to prepare only one verification report per all launches. For example, one of the launch failed with exception, the other found several unsafes and finish with timeout and the last one suddenly proved true. Now there is a restriction, that a safe verdict can not be combined with unsafe or unknown, which is reasonable. Also, there are different resources, logs and so on. It is not correct to put all this data into different attributes of unsafe reports. Thus I still consider the restriction 'only one verification report' as irrelevant.</p>
</blockquote>
<p>Of course, users are interested in verification results first of all. Thus, you need to prepare them in a standard way. For providing data that can be interested for verifier developers there are different means in Klever that I already described. I am not sure that you was aware about them.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354252018-12-13T11:08:40ZPavel Andrianovandrianov@ispras.ru
<ul></ul><blockquote>
<p>For providing data that can be interested for verifier developers there are different means</p>
</blockquote>
<p>I am not speaking about developers. This is a practical issue, when verification task is prepared once and then different configurations are used (memory check with SMG, race check with CPALockator). We do not include any developer-specific features in the report.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354282018-12-13T12:41:23ZVladimir Gratinskiygratinskiy@ispras.ru
<ul></ul><p>Evgeny Novikov wrote:</p>
<blockquote>
<p>Vladimir Gratinskiy wrote:</p>
<blockquote>
<p>Evgeny Novikov wrote:</p>
<blockquote>
<p>As far as I rememember there can be the only verification report for the same parent (Vladimir, am I right?).</p>
</blockquote>
<p>There is no such restriction.</p>
</blockquote>
<p>Okay. Does Bridge compare verification results on the basis of verification reports? That's it calculates a total verdict for a given verification report and all its children?</p>
</blockquote>
<p>It calculates total verdict on the basis of attributes values. Each leaf (unsafe/safe/unknown) has its own attributes that are copied from all parents branch (including verification report).</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354382018-12-14T12:02:40ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Vladimir Gratinskiy wrote:</p>
<blockquote>
<p>Evgeny Novikov wrote:</p>
<blockquote>
<p>Vladimir Gratinskiy wrote:</p>
<blockquote>
<p>Evgeny Novikov wrote:</p>
<blockquote>
<p>As far as I rememember there can be the only verification report for the same parent (Vladimir, am I right?).</p>
</blockquote>
<p>There is no such restriction.</p>
</blockquote>
<p>Okay. Does Bridge compare verification results on the basis of verification reports? That's it calculates a total verdict for a given verification report and all its children?</p>
</blockquote>
<p>It calculates total verdict on the basis of attributes values. Each leaf (unsafe/safe/unknown) has its own attributes that are copied from all parents branch (including verification report).</p>
</blockquote>
<p>I understand that. But I wanted to clarify, how comparison works. If I don't mistake, for each verification report Bridge calculates a total verdict on the basis of its child reports, e.g. "Safe" or "Found all unsafes". And then it compares total verdicts for equal values of attributes that are marked to be used for comparison. Sometimes there may be non-matching attribute values.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=354392018-12-14T12:23:25ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Feedback</i> to <i>Open</i></li></ul><p>Pavel Andrianov wrote:</p>
<blockquote><blockquote>
<p>For providing data that can be interested for verifier developers there are different means</p>
</blockquote>
<p>I am not speaking about developers. This is a practical issue, when verification task is prepared once and then different configurations are used (memory check with SMG, race check with CPALockator). We do not include any developer-specific features in the report.</p>
</blockquote>
<p>It seems that you described the situation inaccurately. Indeed, you have various verification tasks since you check various specifications for target programs. And you prepare different verification reports for different verification tasks where different instances of a verifier are used for solving those tasks. This matches the common Klever workflow exactly. The only difference is that you have the same sources always while Klever usually has different sources for each verification report. The latter is the case for verification of Linux loadable kernel modules, but in other use cases this can differ. That's why I will try to suggest the general solution of this problem.</p>
<p>Let's consider the following example:<br /><pre>
Core report
sources.zip
Component1 report
Component2 report
sources2.zip
Verification1 report
Attributes1 # For instance, "requirement" is "memory safety" in the proper form.
Log1
Resources1
Unsafe1 report
Verification2 report
sources3.zip
Attributes2 # For instance, "requirement" is "concurrency safety" in the proper form.
Log2
Resources2
Unsafe2 report
Unknown2 report
</pre></p>
In this case Bridge should use sources1.zip and sources2.zip together for error traces of "Unsafe1 report", and it should use sources1.zip, sources2.zip and sources3.zip together for error traces of "Unsafe2 report". Using this feature one will be able to report common sources once. Possible caveats:
<ol>
<li>There can be the same source files with the same or different contents at various levels. I suggest to use those sources that are at a more deep level in this case.</li>
<li>Sources can be uploaded just with component or verification start reports. That's why there won't be data misses and data races when required sources for a child report was not uploaded for its parent or they are uploaded concurrently.</li>
<li>Maybe some more tricky issues.</li>
</ol>
<p>Do everybody agree that this is a good feature to be supported?</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=355082019-01-23T06:42:39ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>We suggested a better solution of this issue in a corresponding specification. <a href="https://github.com/17451k/clade/issues/41" class="external">Here</a> is the blocking issue.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=355132019-01-23T10:13:19ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Related to</strong> <i><a class="issue tracker-4 status-5 priority-6 priority-high2 closed" href="/issues/9356">Feature #9356</a>: Do not deploy the same build bases</i> added</li></ul> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=355552019-01-25T12:30:54ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Category</strong> deleted (<del><i>Bridge</i></del>)</li><li><strong>Assignee</strong> changed from <i>Vladimir Gratinskiy</i> to <i>Evgeny Novikov</i></li></ul> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=368642019-09-18T07:49:44ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Open</i> to <i>Resolved</i></li></ul><p>Except for minor issues this is done in branch <em>klever-3.0</em>.</p> Klever - Feature #9414: Reuse archive with source files between different error traces on report uploadinghttps://forge.ispras.ru/issues/9414?journal_id=376972020-01-16T14:00:43ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Resolved</i> to <i>Closed</i></li></ul><p>In master.</p>