Proton tool info module proton.py

[rmetta]

Rewrote the Proton tool info module, based on the feedback from Philipp Wendler.

[rmetta]

We have updated the proton.py by fixing the error in "Check code format".

[PhilippWendler]

Why not have a return everywhere instead of the status variable? Seems easier to follow that way.

[PhilippWendler]

Seems this was overlooked?

[rmetta]

We have fixed this now and committed the fixed version. Actually, we had different error strings in our implementation of Proton. Now, made the error codes in sync with our implementation. Best regards, Ravi

…

On Thu, Nov 2, 2023 at 7:29 PM Philipp Wendler ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In benchexec/tools/proton.py <#952 (comment)>: > + elif run.exit_code.value == 64 and "Usage error!" in output: + status = "INVALID ARGUMENTS" + + elif run.exit_code.value == 6 and "Out of memory" in output: I would like to get confirmation from you that this inconsistency between e.g. TRUE and UNKNOWN is indeed intendend. — Reply to this email directly, view it on GitHub <#952 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABOMAUZMA3KPEONXC5QGU3TYCORLRAVCNFSM6AAAAAA62VNVPGVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMYTOMJQGM3TAMZZGE> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[rmetta]

Thanks, yet again. We removed the checking of output and committed. Right now. the only strings output (as the last output line) by proton are:- TRUE, FALSE(termination), INTERNAL-ERROR and INCONCLUSIVE. We tested proton bash script at our end, and it seems to work fine. Best regards, Ravi

…

On Thu, Nov 2, 2023 at 8:05 PM Philipp Wendler ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In benchexec/tools/proton.py <#952 (comment)>: > + elif run.exit_code.value == 64 and "Usage error!" in output: + status = "INVALID ARGUMENTS" + + elif run.exit_code.value == 6 and "Out of memory" in output: Hm, with the current code there is still inconsistency with regards wo ... in result_str, result_str == ... and ... in output, all three of which have different semantics. Is this intended? Did you test this <https://github.com/sosy-lab/benchexec/blob/main/doc/tool-integration.md#testing-the-tool-integration> ? Note that for future maintainers of this logic it might be useful to have example output lines of the tool here, if it is not as trivial as just a line consisting only of the specific string. — Reply to this email directly, view it on GitHub <#952 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABOMAU23WSRB6IO7RFFHY6DYCOVUVAVCNFSM6AAAAAA62VNVPGVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMYTOMJQGQ3DGMZXGM> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[PhilippWendler]

Ok, but your comment seems to indicate that INCONCLUSIVE is really used as a kind of "result not known" and the code should return RESULT_UNKNOWN, right?

Although, do you think that you will fulfill conditions like run.exit_code.value == 64 and "Usage error!" in output in future versions of Proton? If not, please remove them.

Given all this back and forth and the fact that it now does not look at all anymore like CBMC's output: Is checking for the exit code still relevant?

[rmetta]

1. We have two checks in Proton: one for non-termination (nt-check) and one for termination (t-check). If both of the checks terminate within their respective time slice budget, but both disagree: that is nt-check reports non-termination and t-check reports termination, then we report INCONCLUSIVE. Even though our nt-check is sound, our current tooling has issues (bugs, as well as unsupported complex pointers) and so does our technique (especially in the case of arrays) , due to which the nt-check may give a wrong answer. Where as when Proton reports UNKNOWN, it means that neither t-check, nor nt-check, were successful. So, this distinction is important for us. 2. Cleaned up the error code issue mentioned. And, we are now relying only on strings for outputs. Committed the new version. Thanks and best regards, Ravi

…

On Thu, Nov 2, 2023 at 8:30 PM Philipp Wendler ***@***.***> wrote: Ok, but your comment seems to indicate that INCONCLUSIVE is really used as a kind of "result not known" and the code should return RESULT_UNKNOWN, right? Although, do you think that you will fulfill conditions like run.exit_code.value == 64 and "Usage error!" in output in future versions of Proton? If not, please remove them. Given all this back and forth and the fact that it now does not look at all anymore like CBMC's output: Is checking for the exit code still relevant? — Reply to this email directly, view it on GitHub <#952 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABOMAUY26EPGZM4ABCSHQCLYCOYPDAVCNFSM6AAAAAA62VNVPGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTOOJQHEYDCMZTGE> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[PhilippWendler]

Thanks for the explanation! Then indeed having INCONCLUSIVE as a result of category "error" makes sense.

The new code is also much easier to understand.

[rmetta]

Thanks for your rigorous and timely review. It was a big help. Highly appreciated. Best regards, Ravi

…

On Fri, 3 Nov, 2023, 1:08 pm Philipp Wendler, ***@***.***> wrote: Merged #952 <#952> into main. — Reply to this email directly, view it on GitHub <#952 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABOMAU5OMLOEDIL4EDPPISLYCSNNXAVCNFSM6AAAAAA62VNVPGVHI2DSMVQWIX3LMV45UABCJFZXG5LFIV3GK3TUJZXXI2LGNFRWC5DJN5XDWMJQHA2TEMRWGY2TMNA> . You are receiving this because you authored the thread.Message ID: ***@***.***>