git.iko.soy/Idris-dev
on master help sign in
Extensive bitstring bugfixing
99ed1dbBenjamin Saunders
lib/Prelude/Bits.idr+106−71
compare with master
unifiedsplit
@@ -26,6 +26,28 @@ machineTy (S O) = Bits16
26machineTy (S (S O)) = Bits32
26machineTy (S (S O)) = Bits32
27machineTy (S (S (S _))) = Bits64
27machineTy (S (S (S _))) = Bits64
28
28
29+bitsUsed : Nat -> Nat
30+bitsUsed n = 8 * (2 `power` n)
31+
32+%assert_total
33+natToBits' : machineTy n -> Nat -> machineTy n
34+natToBits' a O = a
35+natToBits' {n=n} a x with n
36+ natToBits' a (S x') | O = natToBits' (prim__addB8 a (prim__intToB8 1)) x'
37+ natToBits' a (S x') | S O = natToBits' (prim__addB16 a (prim__intToB16 1)) x'
38+ natToBits' a (S x') | S (S O) = natToBits' (prim__addB32 a (prim__intToB32 1)) x'
39+ natToBits' a (S x') | S (S (S _)) = natToBits' (prim__addB64 a (prim__intToB64 1)) x'
40+
41+natToBits : Nat -> machineTy n
42+natToBits {n=n} x with n
43+ | O = natToBits' (prim__intToB8 0) x
44+ | S O = natToBits' (prim__intToB16 0) x
45+ | S (S O) = natToBits' (prim__intToB32 0) x
46+ | S (S (S _)) = natToBits' (prim__intToB64 0) x
47+
48+getPad : Nat -> machineTy n
49+getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
50+
29public
51public
30data Bits : Nat -> Type where
52data Bits : Nat -> Type where
31 MkBits : machineTy (nextBytes n) -> Bits n
53 MkBits : machineTy (nextBytes n) -> Bits n
@@ -33,73 +55,43 @@ data Bits : Nat -> Type where
33pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
55pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
34pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
56pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
35 where
57 where
36− pad = (prim__intToB8 (cast (8-n)))
58+ pad = getPad {n=0} n
37
59
38pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
60pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
39pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
61pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
40 where
62 where
41− pad = (prim__intToB16 (cast (16-n)))
63+ pad = getPad {n=1} n
42
64
43pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
65pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
44pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
66pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
45 where
67 where
46− pad = (prim__intToB32 (cast (32-n)))
68+ pad = getPad {n=2} n
47
69
48pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
70pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
49pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
71pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
50 where
72 where
51− pad = (prim__intToB64 (cast (64-n)))
73+ pad = getPad {n=3} n
52
74
53-- These versions only pad the first operand
75-- These versions only pad the first operand
54pad8' : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
76pad8' : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
55pad8' n f x y = prim__lshrB8 (f (prim__shlB8 x pad) y) pad
77pad8' n f x y = prim__lshrB8 (f (prim__shlB8 x pad) y) pad
56 where
78 where
57− pad = (prim__intToB8 (cast (8-n)))
79+ pad = getPad {n=0} n
58
80
59pad16' : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
81pad16' : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
60pad16' n f x y = prim__lshrB16 (f (prim__shlB16 x pad) y) pad
82pad16' n f x y = prim__lshrB16 (f (prim__shlB16 x pad) y) pad
61 where
83 where
62− pad = (prim__intToB16 (cast (16-n)))
84+ pad = getPad {n=1} n
63
85
64pad32' : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
86pad32' : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
65pad32' n f x y = prim__lshrB32 (f (prim__shlB32 x pad) y) pad
87pad32' n f x y = prim__lshrB32 (f (prim__shlB32 x pad) y) pad
66 where
88 where
67− pad = (prim__intToB32 (cast (32-n)))
89+ pad = getPad {n=2} n
68
90
69pad64' : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
91pad64' : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
70pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
92pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
71 where
93 where
72− pad = (prim__intToB64 (cast (64-n)))
94+ pad = getPad {n=3} n
73−
74−%assert_total
75−intToBits' : Int -> machineTy (nextBytes n)
76−intToBits' {n=n} x with (nextBytes n)
77− | O = let pad = (prim__intToB8 (cast (8-n))) in
78− prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
79− | S O = let pad = (prim__intToB16 (cast (16-n))) in
80− prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad
81− | S (S O) = let pad = (prim__intToB32 (cast (32-n))) in
82− prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad
83− | S (S (S _)) = let pad = (prim__intToB64 (cast (64-n))) in
84− prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
85−
86−public
87−intToBits : Int -> Bits n
88−intToBits n = MkBits (intToBits' n)
89−
90−instance Cast Int (Bits n) where
91− cast = intToBits
92−
93−bitsToInt' : machineTy n -> Int
94−bitsToInt' {n=n} x with n
95− | O = prim__B32ToInt (prim__zextB8_32 x)
96− | S O = prim__B32ToInt (prim__zextB16_32 x)
97− | S (S O) = prim__B32ToInt x
98− | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)
99−
100−public
101−bitsToInt : Bits n -> Int
102−bitsToInt (MkBits x) = bitsToInt' x
103
95
104shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
96shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
105shiftLeft' {n=n} x c with (nextBytes n)
97shiftLeft' {n=n} x c with (nextBytes n)
@@ -301,13 +293,13 @@ instance Ord (Bits n) where
301
293
302complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
294complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
303complement' {n=n} x with (nextBytes n)
295complement' {n=n} x with (nextBytes n)
304− | O = let pad = prim__intToB8 (8 - cast n) in
296+ | O = let pad = getPad {n=0} n in
305 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
297 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
306− | S O = let pad = prim__intToB16 (16 - cast n) in
298+ | S O = let pad = getPad {n=1} n in
307 prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad
299 prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad
308− | S (S O) = let pad = prim__intToB32 (32 - cast n) in
300+ | S (S O) = let pad = getPad {n=2} n in
309 prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad
301 prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad
310− | S (S (S _)) = let pad = prim__intToB64 (64 - cast n) in
302+ | S (S (S _)) = let pad = getPad {n=3} n in
311 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
303 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
312
304
313public
305public
@@ -315,7 +307,6 @@ complement : Bits n -> Bits n
315complement (MkBits x) = MkBits (complement' x)
307complement (MkBits x) = MkBits (complement' x)
316
308
317-- TODO: Prove
309-- TODO: Prove
318−%assert_total
319zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
310zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
320zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
311zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
321 | (O, O) = believe_me x
312 | (O, O) = believe_me x
@@ -329,56 +320,100 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
329 | (S (S O), S (S (S _))) = believe_me (prim__zextB32_64 (believe_me x))
320 | (S (S O), S (S (S _))) = believe_me (prim__zextB32_64 (believe_me x))
330 | (S (S (S _)), S (S (S _))) = believe_me x
321 | (S (S (S _)), S (S (S _))) = believe_me x
331
322
332−public partial
323+public
333zeroExtend : Bits n -> Bits (n+m)
324zeroExtend : Bits n -> Bits (n+m)
334zeroExtend (MkBits x) = MkBits (zext' x)
325zeroExtend (MkBits x) = MkBits (zext' x)
335
326
327+%assert_total
328+intToBits' : Int -> machineTy (nextBytes n)
329+intToBits' {n=n} x with (nextBytes n)
330+ | O = let pad = getPad {n=0} n in
331+ prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
332+ | S O = let pad = getPad {n=1} n in
333+ prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad
334+ | S (S O) = let pad = getPad {n=2} n in
335+ prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad
336+ | S (S (S _)) = let pad = getPad {n=3} n in
337+ prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
338+
339+public
340+intToBits : Int -> Bits n
341+intToBits n = MkBits (intToBits' n)
342+
343+instance Cast Int (Bits n) where
344+ cast = intToBits
345+
346+bitsToInt' : machineTy n -> Int
347+bitsToInt' {n=n} x with n
348+ | O = prim__B32ToInt (prim__zextB8_32 x)
349+ | S O = prim__B32ToInt (prim__zextB16_32 x)
350+ | S (S O) = prim__B32ToInt x
351+ | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)
352+
353+public
354+bitsToInt : Bits n -> Int
355+bitsToInt (MkBits x) = bitsToInt' x
356+
336−-- Fill in the high bits of a sign-extended bitstring
357+-- Zero out the high bits of a truncated bitstring
337−fixupSE : (m : Nat) -> machineTy (nextBytes (n+m)) -> machineTy (nextBytes (n+m))
358+zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
338−fixupSE m x = x `or'` complement' (zext' {m=m} (complement' (intToBits' 0)))
359+zeroUnused x = x `and'` complement' (intToBits' 0)
360+
361+instance Cast Nat (Bits n) where
362+ cast x = MkBits (zeroUnused (natToBits n))
339
363
340-- TODO: Prove
364-- TODO: Prove
341−%assert_total
342sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
365sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
343sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
366sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
344− | (O, O) = fixupSE m (believe_me x)
367+ | (O, O) = let pad = getPad {n=0} n in
368+ believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
369+ | (O, S O) = let pad = getPad {n=0} n in
345− | (O, S O) = fixupSE m (believe_me (prim__sextB8_16 (believe_me x)))
370+ believe_me (prim__ashrB16 (prim__sextB8_16 (prim__shlB8 (believe_me x) pad))
371+ (prim__zextB8_16 pad))
372+ | (O, S (S O)) = let pad = getPad {n=0} n in
346− | (O, S (S O)) = fixupSE m (believe_me (prim__sextB8_32 (believe_me x)))
373+ believe_me (prim__ashrB32 (prim__sextB8_32 (prim__shlB8 (believe_me x) pad))
374+ (prim__zextB8_32 pad))
375+ | (O, S (S (S _))) = let pad = getPad {n=0} n in
347− | (O, S (S (S _))) = fixupSE m (believe_me (prim__sextB8_64 (believe_me x)))
376+ believe_me (prim__ashrB64 (prim__sextB8_64 (prim__shlB8 (believe_me x) pad))
348− | (S O, S O) = fixupSE m (believe_me x)
377+ (prim__zextB8_64 pad))
378+ | (S O, S O) = let pad = getPad {n=1} n in
379+ believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)
380+ | (S O, S (S O)) = let pad = getPad {n=1} n in
349− | (S O, S (S O)) = fixupSE m (believe_me (prim__sextB16_32 (believe_me x)))
381+ believe_me (prim__ashrB32 (prim__sextB16_32 (prim__shlB16 (believe_me x) pad))
382+ (prim__zextB16_32 pad))
383+ | (S O, S (S (S _))) = let pad = getPad {n=1} n in
350− | (S O, S (S (S _))) = fixupSE m (believe_me (prim__sextB16_64 (believe_me x)))
384+ believe_me (prim__ashrB64 (prim__sextB16_64 (prim__shlB16 (believe_me x) pad))
351− | (S (S O), S (S O)) = fixupSE m (believe_me x)
385+ (prim__zextB16_64 pad))
386+ | (S (S O), S (S O)) = let pad = getPad {n=2} n in
387+ believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)
388+ | (S (S O), S (S (S _))) = let pad = getPad {n=2} n in
352− | (S (S O), S (S (S _))) = fixupSE m (believe_me (prim__sextB32_64 (believe_me x)))
389+ believe_me (prim__ashrB64 (prim__sextB32_64 (prim__shlB32 (believe_me x) pad))
353− | (S (S (S _)), S (S (S _))) = fixupSE m (believe_me x)
390+ (prim__zextB32_64 pad))
391+ | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
392+ believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
354
393
355−public partial
394+public
356signExtend : Bits n -> Bits (n+m)
395signExtend : Bits n -> Bits (n+m)
357−signExtend (MkBits x) = MkBits (sext' x)
396+signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
358−
359−-- Zero out the high bits of a truncated bitstring
360−fixupTR : machineTy (nextBytes n) -> machineTy (nextBytes n)
361−fixupTR x = x `and'` complement' (intToBits' 0)
362
397
363-- TODO: Prove
398-- TODO: Prove
364−%assert_total
365trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
399trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
366trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
400trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
367− | (O, O) = fixupTR (believe_me x)
401+ | (O, O) = believe_me x
368 | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
402 | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
369 | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))
403 | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))
370 | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))
404 | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))
371− | (S O, S O) = fixupTR (believe_me x)
405+ | (S O, S O) = believe_me x
372 | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))
406 | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))
373 | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))
407 | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))
374− | (S (S O), S (S O)) = fixupTR (believe_me x)
408+ | (S (S O), S (S O)) = believe_me x
375 | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))
409 | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))
376− | (S (S (S _)), S (S (S _))) = fixupTR (believe_me x)
410+ | (S (S (S _)), S (S (S _))) = believe_me x
377
411
378−public partial
412+public
379truncate : Bits (n+m) -> Bits n
413truncate : Bits (n+m) -> Bits n
380−truncate (MkBits x) = MkBits (trunc' x)
414+truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
381
415
416+public
382bitAt : Fin n -> Bits n
417bitAt : Fin n -> Bits n
383bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
418bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
384
419