git.iko.soy/Idris-dev
on master help sign in
Add a test for the C heap.
7932b7fMatus Tejiscak
idris.cabal+7
compare with master
unifiedsplit
@@ -585,6 +585,13 @@ Extra-source-files:
585 test/primitives003/run
585 test/primitives003/run
586 test/primitives003/*.idr
586 test/primitives003/*.idr
587 test/primitives003/expected
587 test/primitives003/expected
588+ test/primitives005/run
589+ test/primitives005/*.idr
590+ test/primitives005/array.c
591+ test/primitives005/array.h
592+ test/primitives005/Data/Bytes.idr
593+ test/primitives005/Data/ByteArray.idr
594+ test/primitives005/expected
588
595
589 test/pkg001/run
596 test/pkg001/run
590 test/pkg001/test.ipkg
597 test/pkg001/test.ipkg
test/Makefile+1−1
@@ -8,7 +8,7 @@ test: $(TESTS)
8 @perl ./runtest.pl $(patsubst %.test,%,$@)
8 @perl ./runtest.pl $(patsubst %.test,%,$@)
9
9
10test_js:
10test_js:
11− @perl ./runtest.pl without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 basic007 basic011 ffi006 --codegen node
11+ @perl ./runtest.pl without primitives005 sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 basic007 basic011 ffi006 --codegen node
12
12
13update:
13update:
14 /usr/bin/env perl ./runtest.pl all -u
14 /usr/bin/env perl ./runtest.pl all -u
test/primitives005/Data/ByteArray.idrnew file+100
@@ -0,0 +1,100 @@
1+module Data.ByteArray
2+
3+%include C "array.h"
4+%link C "array.o"
5+
6+%access public
7+%default total
8+
9+namespace Byte
10+ Byte : Type
11+ Byte = Bits8
12+
13+ toInt : Byte -> Int
14+ toInt = prim__zextB8_Int
15+
16+ fromInt : Int -> Byte
17+ fromInt = prim__truncInt_B8
18+
19+abstract
20+record ByteArray where
21+ constructor BA
22+ ptr : CData
23+ sz : Int
24+
25+-- This needn't be precise; it just needs to be enough to be safe.
26+abstract
27+bytesPerInt : Int
28+bytesPerInt = 8
29+
30+abstract
31+allocate : Int -> IO ByteArray
32+allocate sz = do
33+ ptr <- foreign FFI_C "array_alloc" (Int -> IO CData) sz
34+ return $ BA ptr sz
35+
36+abstract
37+reallocate : Int -> ByteArray -> IO ()
38+reallocate newSz (BA ptr sz)
39+ = foreign FFI_C "array_realloc" (Int -> CData -> IO ()) sz ptr
40+
41+abstract
42+peek : Int -> ByteArray -> IO Byte
43+peek ofs (BA ptr sz)
44+ = if (ofs < 0 || ofs >= sz)
45+ then return 0
46+ else foreign FFI_C "array_peek" (Int -> CData -> IO Byte) ofs ptr
47+
48+abstract
49+peekInt : Int -> ByteArray -> IO Int
50+peekInt ofs (BA ptr sz)
51+ = if (ofs < 0 || ofs+bytesPerInt > sz)
52+ then return 0
53+ else foreign FFI_C "array_peek_int" (Int -> CData -> IO Int) ofs ptr
54+
55+abstract
56+poke : Int -> Byte -> ByteArray -> IO ()
57+poke ofs b (BA ptr sz)
58+ = if (ofs < 0 || ofs >= sz)
59+ then return ()
60+ else foreign FFI_C "array_poke" (Int -> Byte -> CData -> IO ()) ofs b ptr
61+
62+abstract
63+pokeInt : Int -> Int -> ByteArray -> IO ()
64+pokeInt ofs i (BA ptr sz)
65+ = if (ofs < 0 || ofs+bytesPerInt > sz)
66+ then return ()
67+ else foreign FFI_C "array_poke_int" (Int -> Int -> CData -> IO ()) ofs i ptr
68+
69+abstract
70+copy : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO ()
71+copy (BA srcPtr srcSz, srcIx) (BA dstPtr dstSz, dstIx) count
72+ = if (srcIx < 0 || dstIx < 0 || (srcIx+count) > srcSz || (dstIx+count) > dstSz)
73+ then return ()
74+ else foreign FFI_C "array_copy" (CData -> Int -> CData -> Int -> Int -> IO ()) srcPtr srcIx dstPtr dstIx count
75+
76+abstract
77+fill : Int -> Int -> Byte -> ByteArray -> IO ()
78+fill ofs count b (BA ptr sz)
79+ = if (ofs < 0 || ofs+count > sz)
80+ then return ()
81+ else foreign FFI_C "array_fill" (Int -> Int -> Byte -> CData -> IO ()) ofs count b ptr
82+
83+abstract
84+size : ByteArray -> Int
85+size (BA ptr sz) = sz
86+
87+abstract
88+compare : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO Int
89+compare (BA ptrL szL, ofsL) (BA ptrR szR, ofsR) count
90+ = if (ofsL < 0 || ofsL+count > szL || ofsR < 0 || ofsR+count > szR)
91+ then return 0
92+ else foreign FFI_C "array_compare" (CData -> Int -> CData -> Int -> Int -> IO Int) ptrL ofsL ptrR ofsR count
93+
94+abstract
95+find : Byte -> ByteArray -> Int -> Int -> IO (Maybe Int)
96+find b (BA ptr sz) ofs end = do
97+ ofs <- foreign FFI_C "array_find" (Byte -> CData -> Int -> Int -> IO Int) b ptr ofs end
98+ if ofs < 0
99+ then return $ Nothing
100+ else return $ Just ofs
test/primitives005/Data/Bytes.idrnew file+268
@@ -0,0 +1,268 @@
1+module Data.Bytes
2+
3+import Data.ByteArray as BA
4+
5+%access public
6+%default total
7+
8+-- Structure of the allocated ByteArray
9+-- [used_size][.....data.....]
10+-- used_size is an int and it takes up BA.bytesPerInt bytes
11+-- at the beginning of the array
12+
13+abstract
14+record Bytes where
15+ constructor B
16+ arr : ByteArray
17+ ofs : Int
18+ end : Int -- first offset not included in the array
19+
20+minimalCapacity : Int
21+minimalCapacity = 16
22+
23+private
24+dataOfs : Int
25+dataOfs = 1 * BA.bytesPerInt
26+
27+private
28+allocate : Int -> IO Bytes
29+allocate capacity = do
30+ arr <- BA.allocate (BA.bytesPerInt + capacity)
31+ BA.pokeInt 0 dataOfs arr
32+ BA.fill dataOfs capacity 0 arr -- zero the array
33+ return $ B arr dataOfs dataOfs
34+
35+abstract
36+length : Bytes -> Int
37+length (B arr ofs end) = end - ofs
38+
39+abstract
40+empty : Bytes
41+empty = unsafePerformIO $ allocate minimalCapacity
42+
43+abstract
44+null : Bytes -> Bool
45+null (B arr ofs end) = (ofs == end)
46+
47+%freeze empty
48+
49+-- factor=1 ~ copy
50+-- factor=2 ~ grow
51+private
52+grow : Int -> Bytes -> IO Bytes
53+grow factor (B arr ofs end) = do
54+ maxUsed <- BA.peekInt 0 arr
55+ let bytesUsed = end - ofs
56+ let bytesAvailable =
57+ if maxUsed > end
58+ then bytesUsed
59+ else BA.size arr - ofs
60+ B arr' ofs' end' <- allocate $ (factor*bytesAvailable) `max` minimalCapacity
61+ BA.copy (arr, ofs) (arr', ofs') bytesUsed
62+ return $ B arr' ofs' (ofs' + bytesUsed)
63+
64+%assert_total
65+abstract
66+snoc : Bytes -> Byte -> Bytes
67+snoc bs@(B arr ofs end) byte
68+ = if end >= BA.size arr
69+ then unsafePerformIO $ do -- need more space
70+ grown <- grow 2 bs
71+ return $ snoc grown byte
72+ else unsafePerformIO $ do
73+ maxUsed <- BA.peekInt 0 arr
74+ if maxUsed > end
75+ then do -- someone already took the headroom, need copying
76+ copy <- grow 2 bs
77+ return $ snoc copy byte
78+ else do -- can mutate
79+ BA.pokeInt 0 (end+1) arr
80+ BA.poke end byte arr
81+ return $ B arr ofs (end+1)
82+
83+infixl 7 |>
84+(|>) : Bytes -> Byte -> Bytes
85+(|>) = snoc
86+
87+namespace SnocView
88+ data SnocView : Type where
89+ Nil : SnocView
90+ Snoc : (bs : Bytes) -> (b : Byte) -> SnocView
91+
92+ abstract
93+ snocView : Bytes -> SnocView
94+ snocView (B arr ofs end) =
95+ if end == ofs
96+ then SnocView.Nil
97+ else unsafePerformIO $ do
98+ last <- BA.peek (end-1) arr
99+ return $ SnocView.Snoc (B arr ofs (end-1)) last
100+
101+namespace ConsView
102+ data ConsView : Type where
103+ Nil : ConsView
104+ Cons : (b : Byte) -> (bs : Bytes) -> ConsView
105+
106+ abstract
107+ consView : Bytes -> ConsView
108+ consView (B arr ofs end) =
109+ if end == ofs
110+ then ConsView.Nil
111+ else unsafePerformIO $ do
112+ first <- BA.peek ofs arr
113+ return $ ConsView.Cons first (B arr (ofs+1) end)
114+
115+infixr 7 ++
116+%assert_total
117+abstract
118+(++) : Bytes -> Bytes -> Bytes
119+(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)
120+ = let countR = endR - ofsR in
121+ if endL + countR > BA.size arrL
122+ then unsafePerformIO $ do -- need more space
123+ grown <- grow 2 bsL
124+ return $ grown ++ bsR
125+ else unsafePerformIO $ do
126+ maxUsedL <- BA.peekInt 0 arrL
127+ if maxUsedL > endL
128+ then do -- headroom taken
129+ copyL <- grow 2 bsL
130+ return $ copyL ++ bsR
131+ else do -- can mutate
132+ BA.pokeInt 0 (endL + countR) arrL
133+ BA.copy (arrR, ofsR) (arrL, endL) countR
134+ return $ B arrL ofsL (endL + countR)
135+
136+dropPrefix : Int -> Bytes -> Bytes
137+dropPrefix n (B arr ofs end) = B arr (((ofs + n) `min` end) `max` dataOfs) end
138+
139+takePrefix : Int -> Bytes -> Bytes
140+takePrefix n (B arr ofs end) = B arr ofs (((ofs + n) `min` end) `max` dataOfs)
141+
142+pack : List Byte -> Bytes
143+pack = fromList empty
144+ where
145+ fromList : Bytes -> List Byte -> Bytes
146+ fromList bs [] = bs
147+ fromList bs (x :: xs) = fromList (bs `snoc` x) xs
148+
149+unpack : Bytes -> List Byte
150+unpack bs with (consView bs)
151+ | Nil = []
152+ | Cons x xs = x :: unpack (assert_smaller bs xs)
153+
154+slice : Int -> Int -> Bytes -> Bytes
155+slice ofs' end' (B arr ofs end)
156+ = B arr
157+ (((ofs + ofs') `min` end) `max` dataOfs)
158+ (((ofs + end') `min` end) `max` dataOfs)
159+
160+-- Folds with early exit.
161+-- If Bytes were a Functor, this would be equivalent
162+-- to a Traversable implementation interpreted in the Either monad.
163+data Result : Type -> Type where
164+ Stop : (result : a) -> Result a
165+ Cont : (acc : a) -> Result a
166+
167+iterateR : (Byte -> a -> Result a) -> a -> Bytes -> a
168+iterateR f acc bs with (snocView bs)
169+ | Nil = acc
170+ | Snoc ys y with (f y acc)
171+ | Stop result = result
172+ | Cont acc' = iterateR f acc' (assert_smaller bs ys)
173+
174+iterateL : (a -> Byte -> Result a) -> a -> Bytes -> a
175+iterateL f acc bs with (consView bs)
176+ | Nil = acc
177+ | Cons y ys with (f acc y)
178+ | Stop result = result
179+ | Cont acc' = iterateL f acc' (assert_smaller bs ys)
180+
181+infixl 3 .:
182+private
183+(.:) : (a -> b) -> (c -> d -> a) -> (c -> d -> b)
184+(.:) g f x y = g (f x y)
185+
186+foldr : (Byte -> a -> a) -> a -> Bytes -> a
187+foldr f = iterateR (Cont .: f)
188+
189+foldl : (a -> Byte -> a) -> a -> Bytes -> a
190+foldl f = iterateL (Cont .: f)
191+
192+spanLength : (Byte -> Bool) -> Bytes -> Int
193+spanLength p = iterateL step 0
194+ where
195+ step : Int -> Byte -> Result Int
196+ step n b with (p b)
197+ | True = Cont (1 + n)
198+ | False = Stop n
199+
200+find : Byte -> Bytes -> Maybe Int
201+find b (B arr ofs end) = unsafePerformIO $ BA.find b arr ofs end
202+
203+splitAt : Int -> Bytes -> (Bytes, Bytes)
204+splitAt n bs = (takePrefix n bs, dropPrefix n bs)
205+
206+splitOn : Byte -> Bytes -> (Bytes, Bytes)
207+splitOn b bs with (find b bs)
208+ | Nothing = (bs, empty)
209+ | Just ofs = (takePrefix ofs bs, dropPrefix (ofs+1) bs)
210+
211+splitsOn : Byte -> Bytes -> List Bytes
212+splitsOn b bs with (find b bs)
213+ | Nothing = [bs]
214+ | Just ofs = takePrefix ofs bs :: splitsOn b (assert_smaller bs $ dropPrefix (ofs+1) bs)
215+
216+asciiLines : Bytes -> List Bytes
217+asciiLines = splitsOn 0x0A
218+
219+span : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
220+span p bs = splitAt (spanLength p bs) bs
221+
222+break : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
223+break p bs = span (not . p) bs
224+
225+private
226+cmp : Bytes -> Bytes -> Ordering
227+cmp (B arrL ofsL endL) (B arrR ofsR endR) = unsafePerformIO $ do
228+ let countL = endL - ofsL
229+ let countR = endR - ofsR
230+ let commonCount = countL `min` countR
231+ result <- BA.compare (arrL, ofsL) (arrR, ofsR) commonCount
232+ return $
233+ if result /= 0
234+ then i2o result
235+ else compare countL countR
236+ where
237+ i2o : Int -> Ordering
238+ i2o 0 = EQ
239+ i2o i = if i < 0 then LT else GT
240+
241+implementation Eq Bytes where
242+ xs == ys = (Bytes.cmp xs ys == EQ)
243+
244+implementation Ord Bytes where
245+ compare = Bytes.cmp
246+
247+toString : Bytes -> String
248+toString = foldr (strCons . chr . toInt) ""
249+
250+fromString : String -> Bytes
251+fromString = foldl (\bs, c => bs |> fromInt (ord c)) empty . unpack
252+
253+implementation Show Bytes where
254+ show = ("b" ++) . show . toString
255+
256+implementation Semigroup Bytes where
257+ (<+>) = (++)
258+
259+implementation Monoid Bytes where
260+ neutral = empty
261+
262+-- todo:
263+--
264+-- make indices Nats
265+-- Build a ByteString on top of Bytes?
266+-- migrate to (Bits 8)?
267+--
268+-- bidirectional growth?
test/primitives005/array.cnew file+62
@@ -0,0 +1,62 @@
1+#include "array.h"
2+#include <string.h>
3+
4+int array_find(uint8_t byte, CData array, int ofs, int end)
5+{
6+ void * data = array->data + ofs;
7+ void * result = memchr(data, (int) byte, (size_t) (end - ofs));
8+ if (result == NULL)
9+ {
10+ return -1;
11+ }
12+ else
13+ {
14+ return (result - data);
15+ }
16+}
17+
18+void array_realloc(int size, CData array)
19+{
20+ array->data = realloc(array->data, (size_t) size);
21+}
22+
23+CData array_alloc(int size)
24+{
25+ return cdata_allocate((size_t) size, free);
26+}
27+
28+uint8_t array_peek(int ofs, CData array)
29+{
30+ return ((uint8_t *) array->data)[ofs];
31+}
32+
33+void array_poke(int ofs, uint8_t byte, CData array)
34+{
35+ ((uint8_t *) array->data)[ofs] = byte;
36+}
37+
38+int array_peek_int(int ofs, CData array)
39+{
40+ return *((int *) (array->data + ofs));
41+}
42+
43+void array_poke_int(int ofs, int val, CData array)
44+{
45+ *((int *) (array->data + ofs)) = val;
46+}
47+
48+void array_copy(CData src, int src_ofs, CData dst, int dst_ofs, int count)
49+{
50+ // memmove rather than memcpy in case the areas overlap
51+ memmove(dst->data + dst_ofs, src->data + src_ofs, count);
52+}
53+
54+void array_fill(int ofs, int count, uint8_t byte, CData array)
55+{
56+ memset(array->data + ofs, byte, count);
57+}
58+
59+int array_compare(CData l, int lofs, CData r, int rofs, int count)
60+{
61+ return memcmp(l->data + lofs, r->data + rofs, count);
62+}
test/primitives005/array.hnew file+17
@@ -0,0 +1,17 @@
1+#pragma once
2+
3+#include <stdint.h>
4+#include <stddef.h>
5+
6+#include "idris_rts.h"
7+
8+CData array_alloc(int size);
9+void array_realloc(int size, CData array);
10+uint8_t array_peek(int ofs, CData array);
11+int array_peek_int(int ofs, CData array);
12+void array_poke(int ofs, uint8_t byte, CData array);
13+void array_poke_int(int ofs, int i, CData array);
14+void array_copy(CData src, int src_ofs, CData dst, int dst_ofs, int count);
15+void array_fill(int ofs, int count, uint8_t byte, CData array);
16+int array_compare(CData l, int lofs, CData r, int rofs, int count);
17+int array_find(uint8_t byte, CData array, int ofs, int end);
test/primitives005/expectednew file+9
@@ -0,0 +1,9 @@
1+4096
2+("01/8", (145536, 897))
3+("02/8", (145536, 897))
4+("03/8", (145536, 897))
5+("04/8", (145536, 897))
6+("05/8", (145536, 897))
7+("06/8", (145536, 897))
8+("07/8", (145536, 897))
9+("08/8", (145536, 897))
test/primitives005/load-test.idrnew file+47
@@ -0,0 +1,47 @@
1+module Main
2+
3+import Data.Bytes as B
4+import Data.ByteArray as BA
5+
6+%link C "array.o"
7+
8+initialBuf : Bytes
9+initialBuf = pack . concat $ replicate 128 block
10+ where
11+ block : List Byte
12+ block = [10,32,1,10,100,32,1,10,255,32,1,10,1,10,255,32,1,10,255,32,1,10,255,32,1,10]
13+
14+unRLE : Bytes -> Bytes
15+unRLE = fst . iterateL phi (empty, Nothing)
16+ where
17+ phi : (Bytes, Maybe Byte) -> Byte -> Result (Bytes, Maybe Byte)
18+ phi (bs, Nothing) b = Cont (bs, Just b)
19+ phi (bs, Just cnt) b = Cont (bs ++ pack (replicate (cast $ prim__zextB8_Int cnt) b), Nothing)
20+
21+unit : Int -> Byte -> IO ()
22+unit n b =
23+ let expanded = unRLE initialBuf
24+ in let elines = map (flip snoc b) (asciiLines expanded)
25+ in printLn $ (show b ++ "/" ++ show n, length expanded, length elines)
26+
27+alloc : Int -> Int -> IO Int
28+alloc x 0 = return x
29+alloc x i = do
30+ -- allocate an array
31+ arr <- BA.allocate (64 * 1024 * 1024)
32+ -- write "i" at offset 0
33+ BA.pokeInt 0 i arr
34+ -- read number from offset 0
35+ j <- BA.peekInt 0 arr
36+ -- count matches
37+ alloc (x + if i == j then 1 else 0) (i - 1)
38+
39+main : IO ()
40+main = do
41+ -- First allocate 4096 64M arrays to break the C heap if there's a bug
42+ alloc 0 4096 >>= printLn
43+
44+ -- Then, test Bytes
45+ traverse_ (unit n . prim__truncInt_B8) [1..n]
46+ where
47+ n = 8
test/primitives005/runnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env bash
2+cc -c -O2 -o array.o array.c `idris --include`
3+idris $@ -o load-test load-test.idr --nocolour --warnreach
4+./load-test
5+rm -f load-test *.o *.ibc
6+find -name \*.ibc -delete