bisect-binary 0.1 → 0.1.0.1

raw patch · 5 files changed

+53/−10 lines, 5 files

Files

• ChangeLog.md +4/−0
• README.md +1/−1
• bisect-binary.cabal +1/−1
• src/Intervals.hs +17/−4
• src/Main.hs +30/−4

@@ -1,5 +1,9 @@ # Revision history for bisect-binary +## 0.1.0.1++* Fix bugs in `Intervals.hs` found by formal verification with Coq.+ ## 0.1  * First version.

@@ -10,7 +10,7 @@ should be doing. If it does, then you know that the interesting parts are in another part of the file. -`binary-binary` assists in this process by doing the book-keeping and zeroing+`bisect-binary` assists in this process by doing the book-keeping and zeroing out parts of the file.  

@@ -1,5 +1,5 @@ name:                bisect-binary-version:             0.1+version:             0.1.0.1 synopsis:            Determine relevant parts of binary data description:      This little program helps with the following task:

@@ -1,5 +1,16 @@ {-# LANGUAGE LambdaCase, DeriveGeneric #-} +-- |+-- This module provides an (efficient?) (compact?) representation of sets of+-- file offsets, together with a few basic operations.+--+-- The representation is a sorted list of disjoint, non-adjacent intervals.+--+-- The operations 'isEmpty', 'fullIntervals', 'nullInterval', 'subSetOf',+-- 'union', 'intersection' and 'subtract' were formally proven correct using+-- @hs-to-coq@:+-- <https://github.com/antalsz/hs-to-coq/tree/20f8eced04e51289d81ce117861c82c2ea24c4df/examples/intervals>+-- (Three bugs were found in the process.) module Intervals where  import qualified Data.ByteString.Lazy as BS@@ -52,9 +63,11 @@         | to i1 < to i2 = go (i2:is2) (i1:is1)         -- disjoint         | from i1 >= to i2 = go (i1:is1) is2+        -- subset+        | to i1 == to i2 = I f' (to i2) : go is1 is2         -- overlapping         | otherwise = I f' (to i2) : go (i1 { from = to i2} : is1) is2-            where f' = max (from i1) (from i2)+      where f' = max (from i1) (from i2)   union :: Intervals -> Intervals -> Intervals@@ -69,7 +82,7 @@         | from i1 > to i2 = i2 : go (i1:is1) is2         -- overlapping         | otherwise  = go (i1 { from = f'} : is1) is2-            where f' = min (from i1) (from i2)+      where f' = min (from i1) (from i2)  subtract :: Intervals -> Intervals -> Intervals subtract (Intervals is1) (Intervals is2) = Intervals $ go is1 is2@@ -84,12 +97,12 @@         -- i1 contained in i2         | from i2 <= from i1 , to i1 <= to i2 = go is1 (i2:is2)         -- i2 covers beginning of i1-        | from i1 >= from i2 = i1 { from = to i2} : go is1 is2+        | from i1 >= from i2 = go (i1 { from = to i2} : is1) is2         -- i2 covers end of i1         | to i1 <= to i2     = i1 { to = from i2} : go is1 (i2:is2)         -- i2 in the middle of i1         | otherwise = I (from i1) (from i2) :-                      I (to i2)   (to i1) : go is1 is2+                      go (I (to i2) (to i1) : is1) is2   setZeros :: BS.ByteString -> Intervals -> BS.ByteString

@@ -163,8 +163,13 @@                     steps log'                     -- code smell                     liftIO $ exitSuccess+                Just 'F' -> do+                    let log' = log { lgLogs = filter leOk (lgLogs log) }+                    steps log'+                    -- code smell+                    liftIO $ exitSuccess                 Just '?' -> do-                    outputStrLn "Keys: Y: good. N: bad. R: rerun command. U: Undo. Q: Quit"+                    outputStrLn "Keys: Y: good. N: bad. R: rerun command. U: Undo. F: Forget negatives Q: Quit"                     loop                 _ -> loop @@ -179,7 +184,7 @@                 (if done then "" else printf "%7dB new" (size toTry))                 nonZeroBytes                 (if barw > 5 then braille barw len conservative toTry else "")-                (if done then "" else " [YNRUQ?] ")+                (if done then "" else " [YNRUFQ?] ")           -- Single step of the main loop@@ -197,10 +202,31 @@           where             digest = digestLog log +        lastStep :: Log -> InputT IO ()+        lastStep log = fix $ \loop -> do+            getInputChar "Done! [UFQ?]" >>= pure . fmap toUpper >>= \case+                Just 'Q' -> do+                    revert (digestLog log)+                    liftIO $ exitSuccess+                Just 'U' -> do+                    let log' = log { lgLogs = init (lgLogs log) }+                    steps log'+                    -- code smell+                    liftIO $ exitSuccess+                Just 'F' -> do+                    let log' = log { lgLogs = filter leOk (lgLogs log) }+                    steps log'+                    -- code smell+                    liftIO $ exitSuccess+                Just '?' -> do+                    outputStrLn "Keys: U: Undo. F: Forget negatives Q: Quit"+                    loop+                _ -> loop+         -- Main loop         steps log = do-            foldM_ step log (intervalsToTry len)-            outputStrLn $ printf "Done!"+            log' <- foldM step log (intervalsToTry len)+            lastStep log'             -- TODO: What now?