Add validity checks for IntSet and IntMap #456

m-renaud · 2017-12-22T04:58:37Z

Codify the invariants outlined in comments and add property checks to verify that the internal structure of IntSet and IntMap are correct under initial construction, union, intersection, and difference.

This addresses #304.

The checks codify the invariants laid out in the IntSet and IntMap comments. We add validity checks for constructed IntSets and IntMaps as well as union, intersection, and difference operations on them. As it turns out, the mask being a power of 2 checks do not hold for the IntMap implementation; this may be something to investigate.

Also moves this to a where clause to keep it local to the function in which its used.

treeowl

Great work so far! I'd really like a validity check added to the tests for each operation that produces a set/map. Thankfully, strengthening those checks should be a lot easier than what you've already done.

treeowl · 2017-12-22T05:01:11Z

Data/IntMap/Internal.hs

+-- Invariant: Prefix is the common high-order bits that all elements share to
+--            the left of the Mask bit.
+-- Invariant: In Bin prefix mask left right, left consists of the elements that
+--            don't have the mask bit set; right is all the elements that do.


Perhaps explain what a mask looks like?

treeowl · 2017-12-22T05:02:52Z

Data/IntMap/Internal.hs

@@ -3396,3 +3402,50 @@ node = "+--"
 withBar, withEmpty :: [String] -> [String]
 withBar bars   = "|  ":bars
 withEmpty bars = "   ":bars
+


Should these assertions be here or under tests? I'm asking because I don't know.

I was following structure that Data.Set used[1], but I'm open to moving them somewhere else; perhaps in a follow-up PR though.

[1] https://github.com/haskell/containers/blob/master/Data/Set/Internal.hs#L1758

Looking through the implementations I don't think there's anything that requires them to be defined here since the internals of the types are exposed by the Internal module. I think I would prefer to do a mass move across all the data structures in a follow-up though.

treeowl · 2017-12-22T05:04:10Z

Data/IntSet/Internal.hs

-- Invariant: The Prefix is zero for all but the last 5 (on 32 bit arches) or 6
--            bits (on 64 bit arches). The values of the map represented by a tip
+-- Invariant: The Prefix is zero for the last 5 (on 32 bit arches) or 6 bits
+--            (on 64 bit arches). The values of the set represented by a tip


Was this comment just flat-out wrong before? That's confusing and disturbing!

It seems to have been. It took me a little bit to realize that I was implementing the incorrect check :P I went and read the implementation closer and figured that this is I think what it meant to say.

And the test that codifies this interpretation passes, sooo...

m-renaud · 2017-12-22T05:07:09Z

Note to reviewers:

I'm not sure if there's a style guide for the package that I've violated or not. I tried to format things like the surrounding code, feel free to nit pick it though :)
One thing that struck me as strange is that some of the invariants that held for the IntSet relating to properties of the mask and prefix did not hold for the IntMap implementation (or I may have made a mistake porting them over). Specifically the maskPowerOfTwo property did not hold for Mask in the IntMaps Bin constructor. Also, the tipsValid check didn't appear to have a passing analogue.

treeowl · 2017-12-22T05:41:43Z

Sounds good.

…

On Dec 22, 2017 12:31 AM, "Matt Renaud" ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In Data/IntMap/Internal.hs <#456 (comment)>: > @@ -3396,3 +3402,50 @@ node = "+--" withBar, withEmpty :: [String] -> [String] withBar bars = "| ":bars withEmpty bars = " ":bars + I was following structure that Data.Set used[1], but I'm open to moving them somewhere else; perhaps in a follow-up PR though. [1] https://github.com/haskell/containers/blob/master/Data/ Set/Internal.hs#L1758 ------------------------------ In Data/IntMap/Internal.hs <#456 (comment)>: > @@ -3396,3 +3402,50 @@ node = "+--" withBar, withEmpty :: [String] -> [String] withBar bars = "| ":bars withEmpty bars = " ":bars + Looking through the implementations I don't think there's anything that requires them to be defined here since the internals of the types are exposed by the Internal module. I think I would prefer to do a mass move across all the data structures in a follow-up though. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#456 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABzi_dSG_PlSrnneoFFeyLYThXzApw4Dks5tCz6agaJpZM4RKpWc> .

Includes: empty, singleton, insert, delete, fromList, filter, and partition.

m-renaud · 2017-12-22T06:20:34Z

Great work so far!

Thanks! It's been fun ;)

I'd really like a validity check added to the tests for each operation that produces a set/map

Added a bunch more validity checks, see commit for details. Let me know if there's any others you'd like me to add :)

Perhaps explain what a mask looks like?

I've added a short description given what I understand about the implementation, it's a little hand wavey though. #404 would definitely have made this easier ;P

IntSet: split, splitMember IntMap: alter, split

m-renaud · 2017-12-22T17:19:25Z

The CI failures appear to be due to configuration failing and not due to this change.

treeowl · 2017-12-22T17:20:53Z

Ugh. I don't want to hear that! Have you had a chance to look at what invariants you're missing in IntMap?

…

On Dec 22, 2017 12:19 PM, "Matt Renaud" ***@***.***> wrote: The CI failures appear to be due to configuration failing and not due to this change. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#456 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABzi_V6FZ4rFYha2nm1bkoFgYBgY2nvxks5tC-SdgaJpZM4RKpWc> .

m-renaud · 2017-12-22T17:57:08Z

Ugh. I don't want to hear that!

:(

The command "cabal install 'test-framework >= 0.3.3' 'test-framework-quickcheck2 >= 0.2.9' 'QuickCheck >= 2.4.0.1' 'ChasingBottoms' 'HUnit' 'test-framework-hunit'" failed and exited with 1 during .

Have you had a chance to look at what invariants you're missing in IntMap?

Not closely, the implementation is slightly different (wrt keys) than the IntSet implementation. I'll have to take another pass through but I didn't see anything that the code was trying to enforce, there also aren't any comments though so I could very well be missing some.

m-renaud · 2017-12-23T01:49:33Z

Went through the IntMap code again and that looks like all the invariants. Tip is much simpler in the IntMap case since it only ever holds a single (key, value) pair. Let me know if there are any other checks you'd like me to add. If I see anything I missed when making further changes I'll send another PR.

treeowl

Oy. I didn't see what you were doing clearly enough and have now wasted some of your time. I'm sorry. I meant that the validity checks should be incorporated into the other tests. That is, something like

prop_partition :: IntSet -> Int -> Property
prop_partition s i = case partition odd s of
		     (s1,s2) -> valid s1 .&&. valid s2 .&&. (all odd (toList s1) && all even (toList s2)) .&&. s === s1 `union` s2

We also almost certainly want to make valid return a Property so it can explain what was invalid about a bad argument.

m-renaud · 2017-12-23T19:09:10Z

Ah gotcha, no worries, that makes more sense than what I did :)

m-renaud · 2017-12-23T19:15:57Z

We also almost certainly want to make valid return a Property

Absolutely, although having something return a Property living in the Internal module seems weird, which gives more credence to the idea that the valid function maybe shouldn't live where it is today.

tests/ is one option, or we could add a new Data.IntMap.TestUtil in case we decide to expose the internals as a separate package at some point in the future (but its probably best to go with tests/ since there's no concrete plan to export the internals separately).

So, there's two ways to go right now:

Change valid to return a Property (introducing testing code into the actual implementation).
Change it to a Property in the follow-up PR when I move all the valid checks from the various containers to the tests/ directory.

I'm personally leaning towards 2, WDYT?

treeowl · 2017-12-23T19:17:38Z

I'm leaning towards introducing the validity checks for IntMap where we actually want them, and adding a follow-up to do the same for the rest. On Dec 23, 2017 2:15 PM, "Matt Renaud" <[email protected]> wrote: We also almost certainly want to make valid return a Property Absolutely, although having something return a Property living in the Internal module seems weird, which gives more credence to the idea that the valid function maybe shouldn't live where it is today. tests/ is one option, or we could add a new Data.IntMap.TestUtil in case we decide to expose the internals as a separate package at some point in the future (but its probably best to go with tests/ since there's no concrete plan to export the internals separately). So, there's two ways to go right now: 1. Change valid to return a Property (introducing testing code into the actual implementation). 2. Change it to a Property in the follow-up PR when I move all the valid checks from the various containers to the tests/ directory. I'm personally leaning towards 2, WDYT? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#456 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABzi_UtdksTuxn-O1waghCU9QwakM0-Aks5tDVFtgaJpZM4RKpWc> .

m-renaud · 2017-12-23T19:25:55Z

I'm leaning towards introducing the validity checks for IntMap where we
actually want them

Giving it another thought I completely agree, I'll go with that.

- Moves the `valid` function for IntSet and IntMap into tests/IntSetValidity.hs and tests/IntMapValidity. - Make `valid` check inside existing functions instead of introducing new prop_fooValid functions. - Exposes `zero` from IntSet.Internal so it can be used in IntSetValidity.

m-renaud · 2017-12-24T01:28:17Z

Moved the valid function to a new module in the tests/ directory. Is this an OK way to structure it?

treeowl · 2017-12-27T22:48:00Z

I think that's generally okay. I don't know that we really need a separate module, but it shouldn't hurt. However, it shouldn't be a top-level name like that. One option is to add a Data.IntMap.Debug or some such, to include both the validity tests and tree-showing functions.

treeowl · 2017-12-27T22:49:58Z

Er... I guess you're keeping the thing non-exposed from the library? If so, I guess it doesn't matter.

m-renaud · 2017-12-28T00:09:30Z

Yeah, my thought was that if we ever decide to move the internals into their own package to be used by other packages then we can export the validity checks, but since only this package should be messing around with the internals I just created a new module in the tests/ directory. Let me know if that's alright with you or if you'd like me to move them somewhere else.

treeowl · 2017-12-28T00:31:37Z

Sounds fine for now.

…

On Dec 27, 2017 7:09 PM, "Matt Renaud" ***@***.***> wrote: Yeah, my thought was that if we ever decide to move the internals into their own package to be used by other packages then we can export the validity checks, but since only this package should be messing around with the internals I just created a new module in the tests/ directory. Let me know if that's alright with you or if you'd like me to move them somewhere else. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#456 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABzi_WDYmDQHL1r1i2hNhSBNJyBHxUHrks5tEtw6gaJpZM4RKpWc> .

m-renaud · 2017-12-28T02:35:07Z

SGTM. Unless you have any other concerns I think this is ready to merge.

treeowl · 2017-12-28T02:40:14Z

tests/IntMapValidity.hs

+valid t
+  = property (nilNeverChildOfBin t) .&&.
+    property (commonPrefix t) .&&.
+    property (maskRespected t)


I think we probably want to use counterexample rather than property here, to label each type of failure. I wonder if we should push the Property business into commonPrefix and maskRespected so we can see where in the tree the failure lies. That probably shouldn't be necessary for nilNeverChildOfBin, since that will be visually obvious.

Switched to using counterexample for each of these. It would take more work to push Property into the other functions and be done in such a way that we would get actionable information from it, so if its alright with you I'd like to hold off on that for now.

nomeata · 2018-01-18T03:30:33Z

tests/IntSetValidity.hs

+    Nil -> True
+    Tip _ _ -> True
+    Bin _ m l r ->
+      (m `mod` 2 == 0) && maskPowerOfTwo l && maskPowerOfTwo r


I am a bit late to the party, but

m `mod` 2 == 0

is not a way to test that a mask is a power of 2. Alternative: popcount m == 1.

treeowl · 2018-01-18T03:35:08Z

Not late at all. Thanks! On Jan 17, 2018 10:30 PM, "Joachim Breitner" <[email protected]> wrote: *@nomeata* commented on this pull request. ------------------------------ In tests/IntSetValidity.hs <#456 (comment)>:

+ where

+ noNilInSet t' = + case t' of + Nil -> False + Tip _ _ -> True + Bin _ _ l' r' -> noNilInSet l' && noNilInSet r' + +-- Invariant: The Mask is a power of 2. It is the largest bit position at which +-- two elements of the set differ. +maskPowerOfTwo :: IntSet -> Bool +maskPowerOfTwo t = + case t of + Nil -> True + Tip _ _ -> True + Bin _ m l r -> + (m `mod` 2 == 0) && maskPowerOfTwo l && maskPowerOfTwo r I am a bit late to the party, but m `mod` 2 == 0 is not a way to test that a mask is a power of 2. Alternative: popcount m == 1. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#456 (review)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABzi_fLic-dP7GY0MQO1mJF4hC7nEWxOks5tLrrZgaJpZM4RKpWc> .

m-renaud added 2 commits December 21, 2017 20:41

Rename validBinPrefix to sharedPrefix.

a6afb19

Also moves this to a where clause to keep it local to the function in which its used.

treeowl reviewed Dec 22, 2017

View reviewed changes

m-renaud added 2 commits December 21, 2017 22:03

Added validity tests for functions producing IntSets/IntMaps.

2a5f770

Includes: empty, singleton, insert, delete, fromList, filter, and partition.

Add field comments for IntMap Bin constructor.

95ccc3b

Add more validity tests.

aba5a5d

IntSet: split, splitMember IntMap: alter, split

treeowl requested changes Dec 23, 2017

View reviewed changes

Actually remove valid from IntMap.

2e81fb5

m-renaud added the testing label Dec 26, 2017

treeowl reviewed Dec 28, 2017

View reviewed changes

Used counterexample in validity checks.

3008ab9

m-renaud merged commit c3bca8f into haskell:master Dec 30, 2017

m-renaud mentioned this pull request Dec 30, 2017

Consider enforcing Nil restriction in Data.IntMap structurally #225

Closed

m-renaud deleted the validity-checks branch December 30, 2017 23:09

nomeata reviewed Jan 18, 2018

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add validity checks for IntSet and IntMap #456

Add validity checks for IntSet and IntMap #456

m-renaud commented Dec 22, 2017

treeowl left a comment

treeowl Dec 22, 2017

m-renaud Dec 24, 2017

treeowl Dec 22, 2017

m-renaud Dec 22, 2017

m-renaud Dec 22, 2017

treeowl Dec 22, 2017

m-renaud Dec 22, 2017

m-renaud Dec 22, 2017

m-renaud commented Dec 22, 2017

treeowl commented Dec 22, 2017 via email

m-renaud commented Dec 22, 2017

m-renaud commented Dec 22, 2017

treeowl commented Dec 22, 2017 via email

m-renaud commented Dec 22, 2017

m-renaud commented Dec 23, 2017

treeowl left a comment

m-renaud commented Dec 23, 2017

m-renaud commented Dec 23, 2017

treeowl commented Dec 23, 2017 via email

m-renaud commented Dec 23, 2017

m-renaud commented Dec 24, 2017

treeowl commented Dec 27, 2017

treeowl commented Dec 27, 2017

m-renaud commented Dec 28, 2017

treeowl commented Dec 28, 2017 via email

m-renaud commented Dec 28, 2017

treeowl Dec 28, 2017

m-renaud Dec 30, 2017

nomeata Jan 18, 2018

treeowl commented Jan 18, 2018 via email

Add validity checks for IntSet and IntMap #456

Add validity checks for IntSet and IntMap #456

Conversation

m-renaud commented Dec 22, 2017

treeowl left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

m-renaud commented Dec 22, 2017

treeowl commented Dec 22, 2017 via email

m-renaud commented Dec 22, 2017

m-renaud commented Dec 22, 2017

treeowl commented Dec 22, 2017 via email

m-renaud commented Dec 22, 2017

m-renaud commented Dec 23, 2017

treeowl left a comment

Choose a reason for hiding this comment

m-renaud commented Dec 23, 2017

m-renaud commented Dec 23, 2017

treeowl commented Dec 23, 2017 via email

m-renaud commented Dec 23, 2017

m-renaud commented Dec 24, 2017

treeowl commented Dec 27, 2017

treeowl commented Dec 27, 2017

m-renaud commented Dec 28, 2017

treeowl commented Dec 28, 2017 via email

m-renaud commented Dec 28, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

treeowl commented Jan 18, 2018 via email