On Tue, 8 May 2007 15:03:16 +0100
"Neil Mitchell"
Hi,
{- ICFP referees look away now -}
Dons asked me to check some of the StackSet code for potential pattern match errors, and indeed, there are some. I used Catch (http://www-users.cs.york.ac.uk/~ndm/catch/) to do all the testing.
The first thing I had to do was apply a 2 line patch to get that module building with Yhc/nhc, to do with defaulting. Next I ran the program and found:
1) view related:
* view calls error, this clearly makes it possible to crash.
* raiseFocus calls view
2) head related:
* promote calls head, in a potentially unsafe manner
3) tail related:
* swap calls tail, again potentially unsafe. This one is easy to fix, simply use drop 1. This also means that promote could crash due to swap.
4) fromJust related:
index calls fromJust, which means that it may crash. This means that all functions calling index are potentially unsafe, including: delete, insert, promote, push, shift, view, raiseFocus
I took a look at delete, and it looks like the safety depends on the stacks and the cache all agreeing - plus possibly some other invariants. You could probably rewrite some of this code to be more rebust, and gain a proof of safety.
5) everything else:
Everything else is safe, apart from (potentially) the Ord instances passed around - I abstracted them away for the testing of Data.Map. Realistically, I think you are fine on this point. This means you have a proof of pattern match safety for:
screen, peekStack, empty, peek, member, rotate, workspace, visibleWorkspaces
I've applied patches that should fix all of these.
You also have three options regarding Catch use:
1) Integrate the 2 line change, add the Catch module testing framework in so anyone with Catch installed can replicate these tests - and check you don't get worse. 2) Have a catch branch, which has the library driver and the patch. This would be a really small branch :-) 3) Don't do anything, I can continue to check things occasionally.
I'd like to get this in the main repository. Can you send a patch (or some instructions)? Thanks, Spencer Janssen