Skip to content

Def_exc: Fix issues in leq, join, narrow, meet with broken checking for in_range#100

Merged
michael-schwarz merged 7 commits intomasterfrom
def_exc_quickcheck_fixes
Oct 2, 2020
Merged

Def_exc: Fix issues in leq, join, narrow, meet with broken checking for in_range#100
michael-schwarz merged 7 commits intomasterfrom
def_exc_quickcheck_fixes

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz commented Sep 24, 2020 •
edited
Loading

This fixes some of the issues quickcheck (see #99) found for def_exc.

  • leq: between Definite and Excluded did not take the ranges into account
  • join: was too eager to increase the range.
  • meet: checked whether the excluded value on the right was in the range interval instead of checking if it is in the range represented by that interval

It also fixes an issue where narrow was changed by mistake in #97 causing a time-out on some of the regression tests.
It now runs the quickchecks but skips the test for associativity of join, as our join is not associative.

The join i still not associative

Because of the ranges (fixed now)

a: Unknown int([-63,63]) 
b: 0
c: 7317727852

join(a,b) : Unknown int([-63,63]) 
join(join(a,b), c): Unknown int([-63,63])

join(b,c): Unknown int([0,64])
join(join(b,c), a):  Unknown int([-63,64])

This problem comes from having to chose an exclusion range for a join of two definites. Whichever way one does this (so long vs. unsigned long here), this problem will crop up.
I guess one could go to the non-C range of [0,n-1] for values that fit both into the signed and unsigned type of size n.

And more fundamentally

a: Not {1}([-63,63]) 
b: 0
c: -1

join(a,b): Not {1}([-63,63]) 
join(join(a,b),c): Not {1}([-63,63])

join(b,c): Unknown int([-7,7]) 
join(a, join(b,c)): Unknown int([-63,63])

@michael-schwarz michael-schwarz marked this pull request as draft September 24, 2020 13:51
@vesalvojdani
Copy link
Copy Markdown
Member

vesalvojdani commented Sep 24, 2020

These exclusion sets have been explored in this SAS paper. In particular, Example 6 "any minimal quasi-join for the donut domain over intervals is non-associative". I haven't taken a very deep look at what remedies they suggest, but I think a deep read of that paper may be useful.

@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Oct 1, 2020 •
edited
Loading

It seems like the cases from above where analysis does not terminate are unrelated to the arrays, we have the same behavior for this simple example as well:

analyzer/tests/regression/02-base/33-backwards-loop.c

Lines 1 to 10 in 037ac0d

// PARAM: --sets solver td3
void main(void) {
int x;
int i = 41;
while(i >= 12) {
x = 0;
i--;
}
}

The change that causes it to no longer terminate is this one in the meet:

Old

analyzer/src/cdomains/intDomain.ml

Lines 735 to 739 in c5968eb

| `Excluded (x,r1), `Excluded (y,r2) ->
let r' = R.meet r1 r2 in
let in_range i = R.leq (R.of_int i) r' in
let s' = S.union x y |> S.filter in_range in
`Excluded (s', r')

This implementation of in_range is flawed as it will return true only for values that are inside the interval R, but R is the range in bits. Here e.g. meet(Excluded {42} [0,32],Excluded {44} [0,32]} = Excluded {} [0,32] as neither [42,42] <= [0,32] nor [44,44} <= [0,32].

Here it terminates with the following value in line 10:

i -> def_exc:Not {-31, -30, -29, -28, -27, -26, -25, -24, -23, -22, -21, -20, -19, -18, -17, -16, -15, -14, -13, -12, -11, -10, -9, -8, -7, -6, -5, -4, -3, -2, -1}([-31,31])

This is due to starting x and ending x returning Excluded {0} _ for x != 0. In the loop this becomes Excluded {-1} _, on the join with Definite 41, the result remains Excluded{-1} _. Now, for the condition we then have Excluded {-1,0} _ and so on. This continues until we can exclude the entire negative part of the interval (that is also within the bit range).

New

analyzer/src/cdomains/intDomain.ml

Lines 722 to 729 in 037ac0d

let in_range r i =
match min_of_range r with
| None when i < 0L -> true
| Some l when i < 0L -> l <= i
| _ ->
match max_of_range r with
| None -> true
| Some u -> i <= u

analyzer/src/cdomains/intDomain.ml

Lines 786 to 789 in 037ac0d

| `Excluded (x,r1), `Excluded (y,r2) ->
let r' = R.meet r1 r2 in
let s' = S.union x y |> S.filter (in_range r') in
`Excluded (s', r')

This problem is fixed here, but now it takes as many iterations to terminate as there are negative numbers in the interval, so 2^31 in this case.

@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Oct 1, 2020

Changing starting x and ending x to not exclude 0 leads to 2 tests failed: ["04/36 trylock_nr", "04/42 trylock_2mutex"].
Both of those work again if we enable intervals for them.

@vesalvojdani
Copy link
Copy Markdown
Member

vesalvojdani commented Oct 1, 2020 •
edited
Loading

A naive question: why does narrowing for exclusions sets always use the meet operation? That seems like an interval narrowing always improving the result. Maybe just meet (use refined value) if exclusion set is empty, but do not grow it if it contains any elements already. Do we actually need exclusion sets to be refined?

[Edited] I forgot my main question. Simmo had a similar case in his path-sensitive domain where backward looping failed, but forward iteration worked. Are we handling negative numbers differently, or why is this only triggered for x--?

@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Oct 1, 2020

A naive question: why does narrowing for exclusions sets always use the meet operation? That seems like an interval narrowing always improving the result. Maybe just meet (use refined value) if exclusion set is empty, but do not grow it if it contains any elements already. Do we actually need exclusion sets to be refined?

Not so much a naive question as a good one! Looks like we replaced narrow x y = x by narrow = meet when getting rid of StdCousot in e5889b2.
This is obviously not a smart thing to do.

[Edited] I forgot my main question. Simmo had a similar case in his path-sensitive domain where backward looping failed, but forward iteration worked. Are we handling negative numbers differently, or why is this only triggered for x--?

No, it does not have anything to do with negative numbers or iterating backwards per se, we have the same behavior in all of these cases here. It's just that the iterating backwards case is the one that appears most natural out of all of those.

https://github.com/goblint/analyzer/blob/d74e95e89d3e21b003572607c54d526a4b60ca3d/tests/regression/02-base/33-meet-def-exc.c

@michael-schwarz michael-schwarz changed the title Def_exc: Fix issues in leq, join, meet with broken checking for in_range Def_exc: Fix issues in leq, join, narrow, meet with broken checking for in_range Oct 1, 2020
@michael-schwarz michael-schwarz marked this pull request as ready for review October 1, 2020 09:12
@michael-schwarz michael-schwarz mentioned this pull request Oct 1, 2020
Closed
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Oct 1, 2020 •
edited
Loading

I moved the parts that will still be relevant after merging this into #105

@goblint goblint deleted a comment from vesalvojdani Oct 1, 2020
@michael-schwarz michael-schwarz merged commit c357940 into master Oct 2, 2020
@michael-schwarz michael-schwarz deleted the def_exc_quickcheck_fixes branch October 2, 2020 11:59
@michael-schwarz michael-schwarz mentioned this pull request Oct 2, 2020
Merged
@sim642 sim642 mentioned this pull request Apr 15, 2025
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@michael-schwarz @vesalvojdani