Changes for Pull Request bench#85: Automatic Generation of Test Cases for Incremental Static Analysis #1096
Conversation
|
Do we intend to merge this or should we close it? |
|
As far as I know @stilscher meant that she wants to merge it after reviewing. |
|
Yeah, thanks for the answer. The question was indeed mostly directed at her, since there has been no progress here for the last 3 months. |
docs/developer-guide/testing.md
Outdated
| @@ -53,6 +53,8 @@ Comments at the end of other lines indicate the behavior on that line: | |||
| | `DEADLOCK` | Deadlock warning | Deadlock is possible | Soundness | | |||
| | `NOWARN` | No warning | — | Precision | | |||
| | `WARN` | Some warning | — | Soundness | | |||
| | `NOFAIL` | Assertion is unknown <br> or succeeds | Everything except fail | Incremental analysis | | |||
| | `NOTINPRECISE` | Assertion succeeds <br> or fails | Everything except unknown | Incremental analysis <br> precision | | |||
There was a problem hiding this comment.
I think we can assume that precision tests for the incremental analysis are only run when correctness has already been checked. Therefore, I think we can avoid adding the assertion NOIMPRECISE and just expect SUCCESS for checks that succeeded in the from-scratch comparison run. In my opinion this is preferable as the meaning of an assertion that can either fail or succeed is not very clear anyway.
|
Since the number of commits is very large, but only few lines of code have been changed, I would suggest to squash merge this PR after the review is finished. |
| @@ -53,6 +53,7 @@ Comments at the end of other lines indicate the behavior on that line: | |||
| | `DEADLOCK` | Deadlock warning | Deadlock is possible | Soundness | | |||
| | `NOWARN` | No warning | — | Precision | | |||
| | `WARN` | Some warning | — | Soundness | | |||
| | `NOFAIL` | Assertion is unknown <br> or succeeds | Everything except fail | Incremental analysis | | |||
There was a problem hiding this comment.
What's the meaning of "Everything except fail" as concrete semantics? Isn't that just "Assertion succeeds"?
There was a problem hiding this comment.
It may succeed or be unknown. It is what one expects for an incremental run if the assert was proven in a from-scratch run.
There was a problem hiding this comment.
That's in our abstract semantics, but in the concrete the assertion either fails or it succeeds. So it should be "Assertion may both succeed or fail"?
| ### Test Automation for Incremental Analysis - TAIA | ||
| The "Test Automation for Incremental Analysis" in the bench repository (`bench/incremental-analysis-test-toolchain`) enables you to generate and run incremental tests based on one single c file as input. You find more details in the readme file in the repository (`bench/incremental-analysis-test-toolchain/README.md`). |
There was a problem hiding this comment.
This refers to the unmerged goblint/bench#58. If that isn't merged, our documentation probably shouldn't refer people to non-existent things.
There was a problem hiding this comment.
The plan would be to merge it. It is very self-contained, there are few things one would like to change before merging.
| elsif obj =~ /(\b|\/)(assert|__goblint_check).*\(/ then | ||
| unless obj =~ /^\s*extern\b/ |
There was a problem hiding this comment.
It is about an extern definition of 'goblint_check', which would otherwise also be matched.
|
The indentation issues were introduced when merging master and are found in files not related to this PR. |
|
@sim642 In the GobCon today, you mentioned that you want to have a look at this PR and potentially cherry-pick some changes, before closing this. (As we are currently not working on the incremental). |
|
I cherry-picked and generalized the configurability of the assert transformation to |
Changes needed for the "Test Automation for Incremental Analysis - TAIA" from the pull request in the bench repository:
Add new goblint check annotation
NOFAILwhich expresses the knowledge the incremental analysis should have: After an incremental analysis the check should either be successful or unknown, but not fail. TheTODOannotation is similar but not sufficient, as theupdate_suite.rbscript ignores these annotations.Add new goblint check annotation
NOTINPRECISEwhich checks that the incremental analysis did not get less precise. After an incremental analysis the check should either be successful or failing, but not unknown. Failing tests are ignored to only warn in case if inprecision, as we intend to check only for the precision and not the correctness.Add a reference to the "Test Automation for Incremental Analysis - TAIA" in the documentation.
Improve the regex in the
update_suite.rbscript for matching annotations. The annotations are sometimes part of code generated by cil (e.g.SOME_CIL_VARIABLE_FAIL). To prevent false matchings the annotation should start with a word boundary\bor a/for the case that the annotation was written directly after a comment (e.g.//SUCCESS).When there is an exception in the
update_suite.rbprint the content of thewarn-filefor easier debugging.In the
update_suite.rbscript use the// PARAM:string at the first line also for the incremental tests.Add a bool option
trans.goblint-checkfor writing out__goblint_check()s instead of__VERIFIER_asserts.Change the depreciated parameter
--setsin the regression test46/26to--setChange
MAYFAILtoMAY FAILfor regression test 36/86, 58/15 and 67/16. Otherwise theFAILwould not be recognized by the tester due to the changed regex matching of the annoations.