Make octagon based on Apron useable by ivanazuzic · Pull Request #196 · goblint/analyzer

ivanazuzic · 2021-04-22T01:02:54Z

OctApron analysis and OctApronDomain are added
Update_suite.rb distinguishes UNKNOWN (can be unknown) and UNKNOWN! (must be unknown)
Base analysis takes into account the assertion results from other analysis that answer to AssertionResult
AssertionResult is added as a new query
Function signatures regarding ranges of data types are added to the interface of IntDomain.Size
zip is moved from base.ml to goblintutil.ml because it's also used from octApron.ml

This reverts commit 84e397c.

Copied from cpa tests. Revealed by: gobopt='--sets ana.activated[+] octApron' ./scripts/update_suite.rb

sim642 · 2021-05-27T09:31:02Z

OctApron fails two new tests which I extracted from existing non-apron tests:

Expected unknown!, but registered fail on branch:11
    assert(i == 2); // UNKNOWN!
24/19 octagon/branch failed!

Expected unknown!, but registered success on float:16
    assert(top == top); //UNKNOWN!
24/20 octagon/float failed!

branch

In the branch test, the octApron state in the if is flipped from what it should be! It states [|i-1.>=0; -i+1.>=0|] which essentially is i-1==0. In general the branch function isn't flipped (removing a not makes other octApron tests fail). But I think the issue is in this code:

analyzer/src/cdomains/apron/octApronDomain.apron.ml

Lines 272 to 278 in 134fd40

    
           let rec assert_inv d x b = 
        
             try 
        
               (* if assert(x) then convert it to assert(x != 0) *) 
        
               let x = match x with 
        
                 | Lval (Var v,NoOffset) when isArithmeticType v.vtype -> 
        
                 BinOp (Ne, x, (Const (CInt64(Int64.of_int 0, IInt, None))), intType) 
        
                 | _ -> x in

The != 0 extension shouldn't just be done to single variables, but whatever expression. Making it unconditional causes some stack overflow though. Maybe it needs to be somehow conditional like: if it's already a "boolean" expression, don't do it, otherwise do.

This is quite crucial because it's unsound. By constructing the linear constraint from i-1 it by default means i-1==0 if I understand the Apron stuff correctly.

float

I think octApron also tries to handle floats because Apron supposedly does. But it seems like it's oblivious to NaN, causing the same failure as varEq in #141.

sim642

I think it should be in mergeable condition now. The optional Apron dependency and build seems to work. Octagon tests are skipped by default to not cause failures for anyone who doesn't build with Apron. Nevertheless, they can be explicitly executed (using the group "feature") and the CI also builds with Apron and runs them.

I realized just now that because Apron is included in the opam lockfile, such that the CI would install it for testing, it will also be installed thanks to the lockfile via make dev. So any new developers would still have Apron. But the optional dependency means that this PR at least doesn't cause build failures for existing developers. Not sure if we want to change that (remove apron from lockfile and install apron manually in CI script)?

src/util/defaults.ml

vogler · 2021-05-28T09:36:05Z

I realized just now that because Apron is included in the opam lockfile, such that the CI would install it for testing, it will also be installed thanks to the lockfile via make dev. So any new developers would still have Apron.

You mean make deps (and make setup)?
Does Apron have any extra system dependencies?
If it doesn't complicate installation, it's probably fine to have it in the lockfile.
So it's only optional for a release to opam or if someone installs without --locked?
For CI and benchmarks --locked makes sense, but for user installations we could also do without. That would also test if the package constraints are set right. But maybe not worth dealing with if everyone just installs it in a local switch without problems anyway.

michael-schwarz · 2021-05-28T09:38:40Z

Something else that springs to mind:

What is the relationship with the other octagon analysis made by a student when it comes to the tests?
The tests in folder 24 used to be for that, but now octApron somehow reuses them removing any tests for the old one?
Should the tests for octApron not be their own thing (in a new folder) that leave the other tests alone? (At least until we decide to remove the other octagons?)

vogler · 2021-05-28T09:52:44Z

What is the relationship with the other octagon analysis made by a student when it comes to the tests?
The tests in folder 24 used to be for that, but now octApron somehow reuses them removing any tests for the old one?
Should the tests for octApron not be their own thing (in a new folder) that leave the other tests alone? (At least until we decide to remove the other octagons?)

Probably yes.
We should have a way to check the same test with multiple configurations to avoid duplicating files.
Would also be good to run several solvers on the same test. E.g. https://github.com/goblint/analyzer/blob/master/tests/regression/34-localization/01-nested.c should now also be tested with td3 after cf11c4b.

We could just have several lines starting with PARAM: or something like PARAM+: which just appends/overrides the previous config.

sim642 · 2021-05-28T10:01:25Z

You mean make deps (and make setup)?
Does Apron have any extra system dependencies?
If it doesn't complicate installation, it's probably fine to have it in the lockfile.

Sorry, yes, make setup. It has the extra libmpfr-dev system dependency, but that's also listed with make setup (and installed in CI), so that shouldn't be a problem.

So it's only optional for a release to opam or if someone installs without --locked?
For CI and benchmarks --locked makes sense, but for user installations we could also do without. That would also test if the package constraints are set right. But maybe not worth dealing with if everyone just installs it in a local switch without problems anyway.

Yes. User installations being without lockfile is an interesting idea too. Because if everyone's using the lockfile, then no dependency will ever get updated and we end up with unnecessarily ancient (and possibly more buggy) versions of things.

What is the relationship with the other octagon analysis made by a student when it comes to the tests?
The tests in folder 24 used to be for that, but now octApron somehow reuses them removing any tests for the old one?
Should the tests for octApron not be their own thing (in a new folder) that leave the other tests alone? (At least until we decide to remove the other octagons?)

Yes, right now all of them are just used to test octApron instead. I can make the octApron tests a separate copy if that's desired. But realistically I think we won't end up maintaining that octagon analysis anyway. And currently the old apronDomain/poly stuff is also around, but given how octApronDomain/octApron is more or less a fixed copy, the old one should probably get removed as well (and the fixed one generalized to any Apron domain eventually).

We should have a way to check the same test with multiple configurations to avoid duplicating files.

I've thought about this for a while. But the octApron case is further complicated by the fact that the availability and testability of its configuration depends on whether apron is installed.

michael-schwarz · 2021-05-28T11:26:50Z

I can make the octApron tests a separate copy if that's desired.

I would go with this for now, given that afaik we have not tested the octApron for anything but toy examples?

But realistically I think we won't end up maintaining that octagon analysis anyway.

I agree. Once we are happy with octApron we probably want to remove the other one.

Ah, just saw you did that already

michael-schwarz · 2021-05-28T11:35:46Z

src/analyses/apron/octApron.apron.ml

+
+  let branch ctx e b =
+    if D.is_bot ctx.local then
+      D.bot ()


why not raise Deadcode?

To be honest, every one of the transfer functions (already in poly) starts with if D.is_bot ctx.local then D.bot () for some reason. I don't know why this is because transfer functions shouldn't be called on already dead states anyway. For example, we don't do that sort of extra check in base.

Maybe @ivanazuzic knows why (or whether at all) these are necessary.

michael-schwarz and others added 30 commits March 26, 2021 17:07

Add first problematic example

ebff7b0

Add further problematic example

a2d271b

Add further issue with recursion

249fbcf

Add problem overflow

3d27482

Poly is active again, but tests fail

a464720

Remove incorrect printing attempt

82c22e6

Added Octy analysis

8f03f10

Add loop termination tests

497c321

Use octy instead of octagon

a840eab

Remove unused modules

9f72222

Add comments to ApronDomain

9375d69

Remove unecessary comments from a test

8b7dbb3

Change the name octy to octApron

da31a69

Print what happens with linear constraints

31b9b34

Add an octagn test for handling pointers

be8f4e5

Merge branch 'master' of github.com:goblint/analyzer into octagon_apron

9a249ce

Add parameters to a test

2873c13

Attempt to fix asserting

d3fa2c9

Assert differently and recognise unknown functions, work in progress

8882098

Add printing functions

db23563

OctApron doesn't track globals and pointers

047991f

Possible to assert numbers as booleans

cf87659

Base and octagon analysis work together, has bugs

3e17e9a

Octagon doesn't warn anymore

e96e69b

Remove unnecessary UNKNOWN!

7af5e5a

Octagon doesn't handle assertions with int constants

cb1c639

Octagon doesn't ruin the result from base

fb42fba

Octagon doesn't handle casting

be2deb5

Accept more precise results for annotation unknown

faaea5c

Octagon doesn't handle char constants

f4ab236

sim642 mentioned this pull request May 27, 2021

Decide what version of OCaml to support & Fix CI accordingly #184

Closed

sim642 added 5 commits May 27, 2021 11:18

Revert "Remove octApron where it was included explicitly"

5af3d7e

This reverts commit 84e397c.

Skip apron dependent tests by default

1d3fc16

Run skipped octagon regression tests in CI

9fef4d2

Add two failing tests for octApron

890c0e3

Copied from cpa tests. Revealed by: gobopt='--sets ana.activated[+] octApron' ./scripts/update_suite.rb

Run octagon tests sequentially in CI

134fd40

sim642 mentioned this pull request May 27, 2021

Use optional dependency for Z3 #242

Closed

Ivana Zuzic and others added 3 commits May 27, 2021 15:40

Add an option to disable floats in OctApron, true by default

51b56bd

Solve the problem of contitions with no operator

8ea7174

Simplify match in OctApron assert_inv

31864db

sim642 approved these changes May 28, 2021

View reviewed changes

sim642 requested a review from michael-schwarz May 28, 2021 09:16

michael-schwarz reviewed May 28, 2021

View reviewed changes

src/util/defaults.ml Outdated Show resolved Hide resolved

vogler mentioned this pull request May 28, 2021

support multiple configurations per regression test #243

Open

sim642 added 4 commits May 28, 2021 14:20

Copy octApron tests to 36-octapron

a3be5ef

Restore 24-octagon tests from master

3d8d105

Fix CI for octapron

e82a3e2

Renumber 36-octapron tests sequentially

357a55d

michael-schwarz reviewed May 28, 2021

View reviewed changes

michael-schwarz approved these changes May 28, 2021

View reviewed changes

Rename octApron options under ana.octapron

f261d0d

sim642 merged commit 21438cc into master May 28, 2021

sim642 deleted the octagon_apron branch May 28, 2021 12:26

sim642 mentioned this pull request Jul 14, 2021

Undo update_suite ignoring precision difference for UNKNOWN #286

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Make octagon based on Apron useable#196

Make octagon based on Apron useable#196
sim642 merged 129 commits intomasterfrom
octagon_apron

ivanazuzic commented Apr 22, 2021 •

edited

Loading

Uh oh!

sim642 commented May 27, 2021

Uh oh!

sim642 left a comment

Uh oh!

Uh oh!

vogler commented May 28, 2021

Uh oh!

michael-schwarz commented May 28, 2021 •

edited

Loading

Uh oh!

vogler commented May 28, 2021 •

edited

Loading

Uh oh!

sim642 commented May 28, 2021

Uh oh!

michael-schwarz commented May 28, 2021 •

edited

Loading

Uh oh!

michael-schwarz May 28, 2021

Uh oh!

sim642 May 28, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

ivanazuzic commented Apr 22, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sim642 commented May 27, 2021

branch

float

Uh oh!

sim642 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

vogler commented May 28, 2021

Uh oh!

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

Uh oh!

Uh oh!

vogler commented May 28, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sim642 commented May 28, 2021

Uh oh!

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

Uh oh!

Uh oh!

michael-schwarz May 28, 2021

Choose a reason for hiding this comment

Uh oh!

sim642 May 28, 2021

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

ivanazuzic commented Apr 22, 2021 •

edited

Loading

michael-schwarz commented May 28, 2021 •

edited

Loading

vogler commented May 28, 2021 •

edited

Loading

michael-schwarz commented May 28, 2021 •

edited

Loading