Move assert result output from base to separate assert analysis by sim642 · Pull Request #278 · goblint/analyzer

sim642 · 2021-07-12T12:12:29Z

Inspired by #271 (comment) and some points in the GobCon agenda.

Currently this PR is opened with #251 as base to work via EvalInt, but we don't have to merge it there, just wait until #251 is in master and change the base for this.

vogler · 2021-07-12T14:19:31Z

Looking at the changes, it's a bit ugly that we have so many reg. tests using --set ana.activated instead of --sets ana.activated[+]. I guess most just add some analysis.
Maybe sth to change in a sep. PR?

src/analyses/apron/octApron.apron.ml

michael-schwarz · 2021-07-12T17:53:19Z

src/analyses/libraryFunctions.ml

  | `Calloc       of exp * exp
  | `Realloc      of exp * exp
-  | `Assert       of exp
+  | `Assert       of exp * bool * bool (* exp, should_warn?, change? *) (* TODO: change to non-poly variants to inline record can be used *)


Would it not make sense to split this into some sort of GoblintAssert that is e.g. the result of classify __goblint_check, and keep this completely separate from Assert and use Assert only for actual C asserts?

Then one could have a separate analysis for these "regression test" __goblint_check (which is the analysis you started in this PR). For actual assert the default behavior would always be change and there might be a separate analysis that also does the warnings for C-level asserts that do not hold.

This would also make it easy to warn for programs that contain __goblint_check but are run without this "regression assert" analysis, whereas the behavior changing a lot depending on whether the assert analysis is active or not might be confusing for some.

Splitting assert from __goblint_* might be a bit cleaner indeed, but I'll postpone those changes also to after GobCon to have decided what's our plan with all these things.

Splitting this analysis itself also in two (C assert() analysis and our __goblint_* assert analysis) might be too much hair splitting. We have the dbg.regression option, so the same assert analysis could also warn if that's disabled but __goblint_* is called.

sim642 · 2021-07-13T07:36:41Z

Looking at the changes, it's a bit ugly that we have so many reg. tests using --set ana.activated instead of --sets ana.activated[+]. I guess most just add some analysis.
Maybe sth to change in a sep. PR?

Indeed and we've come across this countless times in the last year adding numerous default analyses. In some cases we probably deactivate a default analysis for a particular test instead. Previously this required a manual listing but since #171 it's also possible to deactivate one, so that's no longer a restriction.

One just needs to go over all these cases and determine, which analyses is the explicit list enabling or disabling compared to the default. Better to leave it as a separate task indeed.

sim642 · 2021-07-13T15:56:07Z

After making the assert() refine by default, running regression tests reveals which tests actually rely on that behavior and which don't. If contradictory conditions are sequentially checked that shouldn't refine under the old behavior, then the contradictory refinements lead to dead code, which then causes "registered nothing" instead of seeing any desired regression testing output.

Thus the sem.assert.refine option is disabled just in those tests. And parts of those could be switched to use __goblint_check instead if wanted.

sim642 · 2021-07-13T16:01:22Z

So if we improve precision somewhere (e.g. by enabling interval which is not on by default), we might get lots of spurious fails because it depends on the old semantics of assert but we didn't identify them here.

If we improve precision of something that isn't already marked as // TODO, then it would fail anyway and require manual attention.

Floats return `Top

sim642 · 2022-07-27T16:09:32Z

I have now split and rebased this as discussed at GobCon:

Assertion check result printing is now done by a separate analysis.
All asserts in tests have been replaced with __goblint_check.
assert (and __goblint_assert) under the hood are now independent of dbg.debug: they always warn and refine when sem.assert.refine is enabled (which it is by default).
Apron analysis now also refines on compatible kinds of assertions. (This will probably allow simplifying some apron tests that previously had to use ifs to set up desired abstract states, but that's now done here.)
Fixes update_suite.rb to actually check __goblint_check!
Adds goblint.h, which is included by default, with the function declarations. This is necessary such that CIL would insert appropriate cast for the argument (if it isn't integral).
Renames __goblint_commit → __goblint_assume, which is a more standard name.

Enjoy reviewing this PR!

Assume is a more standard name, e.g. used in SV-COMP and Dafny.

michael-schwarz · 2022-07-28T08:27:23Z

Enjoy reviewing this PR!

Wasn't so bad given that the changes to the tests all were just mechanical!

From #278.

sim642 added the cleanup Refactoring, clean-up label Jul 12, 2021

sim642 mentioned this pull request Jul 12, 2021

Remove Assert query #251

Merged

michael-schwarz reviewed Jul 12, 2021

View reviewed changes

src/analyses/apron/octApron.apron.ml Outdated Show resolved Hide resolved

michael-schwarz reviewed Jul 12, 2021

View reviewed changes

Base automatically changed from removing_assertion_result to master July 13, 2021 08:41

This was referenced Jul 14, 2021

Base invariant can worsen precision #285

Closed

Undo update_suite ignoring precision difference for UNKNOWN #286

Merged

sim642 marked this pull request as ready for review September 14, 2021 17:56

sim642 mentioned this pull request May 2, 2022

Add option to compile and run regression tests to sanity check assertions #714

Closed

sim642 mentioned this pull request Jul 25, 2022

Replace custom assert declaration with macro #645

Merged

sim642 added 14 commits July 27, 2022 17:18

Move assert result output from base to separate assert analysis

ecf123a

Add assert analysis to all tests with explicit ana.activated

71950e1

Fix query_evalint for floats

10a2c9c

Floats return `Top

Add test where octApron assert should refine

e5ec294

Add assert support to apron

c894142

Remove should_warn argument from base & apron assert_fn

03f5081

Move assert should_warn & change into LibraryFunctions

6fee706

Replace assert -> __goblint_check in tests

88e28cb

Include __goblint function declarations

df38ba0

Fix update_suite.rb not handling __goblint_check

01aca32

Restore intent of 00-sanity/31-assert-redefine

95e1a7c

Add option sem.assert.refine with default value true

f667b43

Make __goblint_assert always warn

f796ef7

Rename library Assert fields to check and refine

c0442a3

sim642 force-pushed the assert-analysis branch from c05ca02 to c0442a3 Compare July 27, 2022 16:00

sim642 requested a review from michael-schwarz July 27, 2022 16:09

sim642 added this to the v2.0.0 milestone Jul 27, 2022

sim642 added 3 commits July 27, 2022 19:15

Add assert analysis to two forgotten 24-octagon tests

c599477

Rename __goblint_commit -> __goblint_assume

fd52938

Assume is a more standard name, e.g. used in SV-COMP and Dafny.

Add separate tests for assert and __goblint_check

52bdd5a

sim642 mentioned this pull request Jul 28, 2022

Fix some asserts in tests #797

Merged

sim642 added the testing label Jul 28, 2022

sim642 mentioned this pull request Jul 28, 2022

Remove explicit ana.activated lists in tests #798

Closed

michael-schwarz approved these changes Jul 28, 2022

View reviewed changes

sim642 merged commit 95ba94f into master Jul 28, 2022

sim642 deleted the assert-analysis branch July 28, 2022 09:59

sim642 mentioned this pull request Aug 4, 2022

Polish __goblint_check #814

Closed

7 tasks

sim642 added a commit that referenced this pull request Oct 4, 2022

Undo accidental ldv_assert -> ldv___goblint_check rename

3800178

From #278.

sim642 added a commit that referenced this pull request Oct 4, 2022

Undo accidental ldv_assert -> ldv___goblint_check rename

1b0cbf7

From #278.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Move assert result output from base to separate assert analysis#278

Move assert result output from base to separate assert analysis#278
sim642 merged 17 commits intomasterfrom
assert-analysis

sim642 commented Jul 12, 2021

Uh oh!

vogler commented Jul 12, 2021

Uh oh!

Uh oh!

michael-schwarz Jul 12, 2021 •

edited

Loading

Uh oh!

michael-schwarz Jul 12, 2021

Uh oh!

sim642 Jul 13, 2021

Uh oh!

sim642 commented Jul 13, 2021

Uh oh!

sim642 commented Jul 13, 2021

Uh oh!

sim642 commented Jul 13, 2021

Uh oh!

sim642 commented Jul 27, 2022 •

edited

Loading

Uh oh!

michael-schwarz commented Jul 28, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

sim642 commented Jul 12, 2021

Uh oh!

vogler commented Jul 12, 2021

Uh oh!

Uh oh!

michael-schwarz Jul 12, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

michael-schwarz Jul 12, 2021

Choose a reason for hiding this comment

Uh oh!

sim642 Jul 13, 2021

Choose a reason for hiding this comment

Uh oh!

sim642 commented Jul 13, 2021

Uh oh!

sim642 commented Jul 13, 2021

Uh oh!

sim642 commented Jul 13, 2021

Uh oh!

sim642 commented Jul 27, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

michael-schwarz commented Jul 28, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

michael-schwarz Jul 12, 2021 •

edited

Loading

sim642 commented Jul 27, 2022 •

edited

Loading