git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2903 from ziman/c-heap
9467e61Niklas Larsson
docs/reference/misc.rst+108−1
compare with master
unifiedsplit
@@ -100,6 +100,113 @@ follows:
100 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))))
100 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))))
101
101
102
102
103+C heap
104+======
105+
106+Idris has two heaps where objects can be allocated:
107+
108++--------------------------------------+---------------------------------------+
109+| FP heap | C heap |
110++======================================+=======================================+
111+| Cheney-collected | Mark-and-sweep-collected |
112++--------------------------------------+---------------------------------------+
113+| Garbage collections touches only | Garbage collection has to traverse |
114+| live objects. | all registered items. |
115++--------------------------------------+---------------------------------------+
116+| Ideal for FP-style rapid allocation | Ideal for C-style allocation of a few |
117+| of lots of small short-lived pieces | big buffers. |
118+| of memory, such as data constructors.| |
119++--------------------------------------+---------------------------------------+
120+| Finalizers are impossible to support | Items have finalizers that are called |
121+| reasonably. | on deallocation. |
122++--------------------------------------+---------------------------------------+
123+| Data is copied all the time (when | Copying does not happen. |
124+| collecting garbage, modifying data, | |
125+| registering managed pointers, etc.) | |
126++--------------------------------------+---------------------------------------+
127+| Contains objects of various types. | Contains C heap items: ``(void *)`` |
128+| | pointers with finalizers. A finalizer |
129+| | is a routine that deallocates the |
130+| | resources associated with the item. |
131++--------------------------------------+---------------------------------------+
132+| Fixed set of object types. | The data pointer may point |
133+| | to anything, as long as the finalizer |
134+| | cleans up correctly. |
135++--------------------------------------+---------------------------------------+
136+| Not suitable for C resources and | Suitable for C resources and arbitrary|
137+| arbitrary pointers. | pointers. |
138++--------------------------------------+---------------------------------------+
139+| Values form a compact memory block. | Items are kept in a linked list. |
140++--------------------------------------+---------------------------------------+
141+| Any Idris value, most notably | Items represented by the |
142+| ``ManagedPtr``. | Idris type ``CData``. |
143++--------------------------------------+---------------------------------------+
144+| Data of ``ManagedPtr`` allocated | Data allocated in C, pointer copied |
145+| in C, buffer then copied into the FP | into the C heap. |
146+| heap. | |
147++--------------------------------------+---------------------------------------+
148+| Allocation and reallocation not | Allocated and reallocate freely in C, |
149+| possible from C code (without having | registering the allocated items |
150+| a reference to the VM). Everything | in the FFI. |
151+| is copied instead. | |
152++--------------------------------------+---------------------------------------+
153+
154+The FP heap is the primary heap. It may contain values of type ``CData``,
155+which are references to items in the C heap. A C heap item contains
156+a ``(void *)`` pointer and the corresponding finalizer. Once a C heap item
157+is no longer referenced from the FP heap, it is marked as unused and
158+the next GC sweep will call its finalizer and deallocate it.
159+
160+There is no Idris interface for ``CData`` other than its type and FFI.
161+
162+Usage from C code
163+-----------------
164+
165+* Although not enforced in code, ``CData`` is meant to be opaque
166+ and non-RTS code (such as libraries or C bindings) should
167+ access only its ``(void *)`` field called ``data``.
168+
169+* Feel free to mutate both the pointer ``data`` (eg. after calling ``realloc``)
170+ and the memory it points to. However, keep in mind
171+ that this must not break Idris's referential transparency.
172+
173+* **WARNING!** If you call ``cdata_allocate`` or ``cdata_manage``,
174+ the resulting ``CData`` object *must* be returned from your
175+ FFI function so that it is inserted in the C heap by the RTS.
176+ Otherwise the memory will be leaked.
177+
178+.. code:: idris
179+
180+ some_allocating_fun : Int -> IO CData
181+ some_allocating_fun i = foreign FFI_C "some_allocating_fun" (Int -> IO CData) i
182+
183+ other_fun : CData -> Int -> IO Int
184+ other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i
185+
186+.. code:: cpp
187+
188+ #include "idris_rts.h"
189+
190+ static void finalizer(void * data)
191+ {
192+ MyStruct * ptr = (MyStruct *) data;
193+ free_something(ptr->something);
194+ free(ptr);
195+ }
196+
197+ CData some_allocating_fun(int arg)
198+ {
199+ void * data = (void *) malloc(...);
200+ // ...
201+ return cdata_manage(data, finalizer);
202+ }
203+
204+ int other_fun(CData cd, int arg)
205+ {
206+ int result = foo(cd->data);
207+ return result;
208+ }
209+
103Preorder reasoning
210Preorder reasoning
104==================
211==================
105
212
@@ -118,7 +225,7 @@ Here is an example:
118 (a * b * c) ={ sym (multAssociative a b c) }=
225 (a * b * c) ={ sym (multAssociative a b c) }=
119 (a * (b * c)) ={ cong (multCommutative b c) }=
226 (a * (b * c)) ={ cong (multCommutative b c) }=
120 (a * (c * b)) ={ multAssociative a c b }=
227 (a * (c * b)) ={ multAssociative a c b }=
121− (a * c * b) ={ cong {f = (*b)} (multCommutative a c) }=
228+ (a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=
122 (c * a * b) QED
229 (c * a * b) QED
123
230
124Note that the parentheses are required -- only a simple expression can
231Note that the parentheses are required -- only a simple expression can
idris.cabal+8
@@ -609,6 +609,14 @@ Extra-source-files:
609 test/primitives005/*.idr
609 test/primitives005/*.idr
610 test/primitives005/expected
610 test/primitives005/expected
611
611
612+ test/primitives006/run
613+ test/primitives006/array.c
614+ test/primitives006/array.h
615+ test/primitives006/load-test.idr
616+ test/primitives006/Data/Bytes.idr
617+ test/primitives006/Data/ByteArray.idr
618+ test/primitives006/expected
619+
612 test/pkg001/run
620 test/pkg001/run
613 test/pkg001/test.ipkg
621 test/pkg001/test.ipkg
614 test/pkg001/*.idr
622 test/pkg001/*.idr
libs/prelude/Builtins.idr+1
@@ -184,6 +184,7 @@ Float = Double
184
184
185export data Ptr : Type
185export data Ptr : Type
186export data ManagedPtr : Type
186export data ManagedPtr : Type
187+export data CData : Type
187
188
188%extern prim__readFile : prim__WorldType -> Ptr -> String
189%extern prim__readFile : prim__WorldType -> Ptr -> String
189%extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int
190%extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int
libs/prelude/IO.idr+1
@@ -178,6 +178,7 @@ namespace FFI_C
178 C_Any : C_Types (Raw a)
178 C_Any : C_Types (Raw a)
179 C_FnT : C_FnTypes t -> C_Types (CFnPtr t)
179 C_FnT : C_FnTypes t -> C_Types (CFnPtr t)
180 C_IntT : C_IntTypes i -> C_Types i
180 C_IntT : C_IntTypes i -> C_Types i
181+ C_CData : C_Types CData
181
182
182 ||| A descriptor for the C FFI. See the constructors of `C_Types`
183 ||| A descriptor for the C FFI. See the constructors of `C_Types`
183 ||| and `C_IntTypes` for the concrete types that are available.
184 ||| and `C_IntTypes` for the concrete types that are available.
rts/idris_gc.c+7
@@ -60,6 +60,10 @@ VAL copy(VM* vm, VAL x) {
60 memcpy(cl, x, size);
60 memcpy(cl, x, size);
61 }
61 }
62 break;
62 break;
63+ case CDATA:
64+ cl = MKCDATAc(vm, x->info.c_heap_item);
65+ c_heap_mark_item(x->info.c_heap_item);
66+ break;
63 default:
67 default:
64 break;
68 break;
65 }
69 }
@@ -133,6 +137,9 @@ void idris_gc(VM* vm) {
133 vm->heap.size += vm->heap.growth;
137 vm->heap.size += vm->heap.growth;
134 }
138 }
135
139
140+ // finally, sweep the C heap
141+ c_heap_sweep(&vm->c_heap);
142+
136 STATS_LEAVE_GC(vm->stats, vm->heap.size, vm->heap.next - vm->heap.heap)
143 STATS_LEAVE_GC(vm->stats, vm->heap.size, vm->heap.next - vm->heap.heap)
137 HEAP_CHECK(vm)
144 HEAP_CHECK(vm)
138}
145}
rts/idris_heap.c+101−1
@@ -1,12 +1,112 @@
1#include "idris_heap.h"
1#include "idris_heap.h"
2#include "idris_rts.h"
2#include "idris_rts.h"
3+#include "idris_gc.h"
3
4
4#include <stdlib.h>
5#include <stdlib.h>
5#include <stddef.h>
6#include <stddef.h>
6#include <stdio.h>
7#include <stdio.h>
8+#include <assert.h>
7
9
10+static void c_heap_free_item(CHeap * heap, CHeapItem * item)
11+{
12+ assert(item->size <= heap->size);
13+ heap->size -= item->size;
14+
15+ // fix links
16+ if (item->next != NULL)
17+ {
18+ item->next->prev_next = item->prev_next;
19+ }
20+ *(item->prev_next) = item->next;
21+
22+ // free payload
23+ item->finalizer(item->data);
24+
25+ // free item struct
26+ free(item);
27+}
28+
29+CHeapItem * c_heap_create_item(void * data, size_t size, CDataFinalizer * finalizer)
30+{
31+ CHeapItem * item = (CHeapItem *) malloc(sizeof(CHeapItem));
32+
33+ item->data = data;
34+ item->size = size;
35+ item->finalizer = finalizer;
36+ item->is_used = false;
37+ item->next = NULL;
38+ item->prev_next = NULL;
39+
40+ return item;
41+}
42+
43+void c_heap_insert_if_needed(VM * vm, CHeap * heap, CHeapItem * item)
44+{
45+ if (item->prev_next != NULL) return; // already inserted
46+
47+ if (heap->first != NULL)
48+ {
49+ heap->first->prev_next = &item->next;
50+ }
51+
52+ item->prev_next = &heap->first;
53+ item->next = heap->first;
54+
55+ heap->first = item;
56+
57+ // at this point, links are done; let's calculate sizes
58+
59+ heap->size += item->size;
60+ if (heap->size >= heap->gc_trigger_size)
61+ {
62+ item->is_used = true; // don't collect what we're inserting
63+ idris_gc(vm);
64+ }
65+}
66+
67+void c_heap_mark_item(CHeapItem * item)
68+{
69+ item->is_used = true;
70+}
71+
72+void c_heap_sweep(CHeap * heap)
73+{
74+ CHeapItem * p = heap->first;
75+ while (p != NULL)
76+ {
77+ if (p->is_used)
78+ {
79+ p->is_used = false;
80+ p = p->next;
81+ }
82+ else
83+ {
84+ CHeapItem * unused_item = p;
85+ p = p->next;
86+
87+ c_heap_free_item(heap, unused_item);
88+ }
89+ }
90+
91+ heap->gc_trigger_size = C_HEAP_GC_TRIGGER_SIZE(heap->size);
92+}
93+
94+void c_heap_init(CHeap * heap)
95+{
96+ heap->first = NULL;
97+ heap->size = 0;
98+ heap->gc_trigger_size = C_HEAP_GC_TRIGGER_SIZE(heap->size);
99+}
100+
101+void c_heap_destroy(CHeap * heap)
102+{
103+ while (heap->first != NULL)
104+ {
105+ c_heap_free_item(heap, heap->first); // will update heap->first via the backward link
106+ }
107+}
8
108
9−/* Used for initializing the heap. */
109+/* Used for initializing the FP heap. */
10void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)
110void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)
11{
111{
12 char * mem = malloc(heap_size);
112 char * mem = malloc(heap_size);
rts/idris_heap.h+82
@@ -1,8 +1,90 @@
1#ifndef _IDRIS_HEAP_H
1#ifndef _IDRIS_HEAP_H
2#define _IDRIS_HEAP_H
2#define _IDRIS_HEAP_H
3
3
4+#include <stdbool.h>
4#include <stddef.h>
5#include <stddef.h>
5
6
7+/* *** C heap ***
8+ * Objects with finalizers. Mark&sweep-collected.
9+ *
10+ * The C heap is implemented as a doubly linked list
11+ * of pointers coupled with their finalizers.
12+ */
13+
14+struct VM;
15+
16+#define C_HEAP_GC_TRIGGER_SIZE(heap_size) \
17+ (heap_size < 2048 \
18+ ? 4096 \
19+ : 2 * heap_size \
20+ )
21+
22+typedef void CDataFinalizer(void *);
23+
24+typedef struct CHeapItem {
25+ /// Payload.
26+ void * data;
27+
28+ /// Size of the item, in bytes.
29+ /// This does not have to be a precise size. It is used to assess
30+ /// whether the heap needs garbage collection.
31+ size_t size;
32+
33+ /// Finalizer that will be called on the payload pointer.
34+ /// Its job is to deallocate all associated resources,
35+ /// including the memory pointed to by `data` (if any).
36+ CDataFinalizer * finalizer;
37+
38+ /// The mark bit set by the FP heap traversal,
39+ /// cleared by C heap sweep.
40+ bool is_used;
41+
42+ /// Next item in the C heap.
43+ struct CHeapItem * next;
44+
45+ /// Pointer to the previous next-pointer.
46+ struct CHeapItem ** prev_next;
47+} CHeapItem;
48+
49+typedef struct CHeap {
50+ /// The first item in the heap. NULL if the heap is empty.
51+ CHeapItem * first;
52+
53+ /// Total size of the heap. (Sum of sizes of items.)
54+ /// This may not be a precise size since individual items'
55+ /// sizes may be just estimates.
56+ size_t size;
57+
58+ /// When heap reaches this size, GC will be triggered.
59+ size_t gc_trigger_size;
60+} CHeap;
61+
62+/// Create a C heap.
63+void c_heap_init(CHeap * c_heap);
64+
65+/// Destroy the given C heap. Will not deallocate the given pointer.
66+/// Will call finalizers & deallocate all blocks in the heap.
67+void c_heap_destroy(CHeap * c_heap);
68+
69+/// Insert the given item into the heap if it's not there yet.
70+/// The VM pointer is needed because this operation may trigger GC.
71+void c_heap_insert_if_needed(struct VM * vm, CHeap * c_heap, CHeapItem * item);
72+
73+/// Mark the given item as used.
74+void c_heap_mark_item(CHeapItem * item);
75+
76+/// Sweep the C heap, finalizing and freeing unused blocks.
77+void c_heap_sweep(CHeap * c_heap);
78+
79+/// Create a C heap item from its payload, size estimate, and finalizer.
80+/// The size does not have to be precise but it should roughly reflect
81+/// how big the item is for GC to work effectively.
82+CHeapItem * c_heap_create_item(void * data, size_t size, CDataFinalizer * finalizer);
83+
84+/* *** Idris heap **
85+ * Objects without finalizers. Cheney-collected.
86+ */
87+
6typedef struct {
88typedef struct {
7 char* next; // Next allocated chunk. Should always (heap <= next < end).
89 char* next; // Next allocated chunk. Should always (heap <= next < end).
8 char* heap; // Point to bottom of heap
90 char* heap; // Point to bottom of heap
rts/idris_rts.c+30
@@ -35,6 +35,8 @@ VM* init_vm(int stack_size, size_t heap_size,
35
35
36 alloc_heap(&(vm->heap), heap_size, heap_size, NULL);
36 alloc_heap(&(vm->heap), heap_size, heap_size, NULL);
37
37
38+ c_heap_init(&vm->c_heap);
39+
38 vm->ret = NULL;
40 vm->ret = NULL;
39 vm->reg1 = NULL;
41 vm->reg1 = NULL;
40#ifdef HAS_PTHREAD
42#ifdef HAS_PTHREAD
@@ -116,6 +118,7 @@ Stats terminate(VM* vm) {
116#endif
118#endif
117 free(vm->valstack);
119 free(vm->valstack);
118 free_heap(&(vm->heap));
120 free_heap(&(vm->heap));
121+ c_heap_destroy(&(vm->c_heap));
119#ifdef HAS_PTHREAD
122#ifdef HAS_PTHREAD
120 pthread_mutex_destroy(&(vm -> inbox_lock));
123 pthread_mutex_destroy(&(vm -> inbox_lock));
121 pthread_mutex_destroy(&(vm -> inbox_block));
124 pthread_mutex_destroy(&(vm -> inbox_block));
@@ -132,6 +135,17 @@ Stats terminate(VM* vm) {
132 return stats;
135 return stats;
133}
136}
134
137
138+CData cdata_allocate(size_t size, CDataFinalizer finalizer)
139+{
140+ void * data = (void *) malloc(size);
141+ return cdata_manage(data, size, finalizer);
142+}
143+
144+CData cdata_manage(void * data, size_t size, CDataFinalizer finalizer)
145+{
146+ return c_heap_create_item(data, size, finalizer);
147+}
148+
135void idris_requireAlloc(size_t size) {
149void idris_requireAlloc(size_t size) {
136#ifdef HAS_PTHREAD
150#ifdef HAS_PTHREAD
137 VM* vm = pthread_getspecific(vm_key);
151 VM* vm = pthread_getspecific(vm_key);
@@ -272,6 +286,22 @@ char* GETSTROFF(VAL stroff) {
272 return (root->str->info.str + root->offset);
286 return (root->str->info.str + root->offset);
273}
287}
274
288
289+VAL MKCDATA(VM* vm, CHeapItem * item) {
290+ c_heap_insert_if_needed(vm, &vm->c_heap, item);
291+ Closure* cl = allocate(sizeof(Closure), 0);
292+ SETTY(cl, CDATA);
293+ cl->info.c_heap_item = item;
294+ return cl;
295+}
296+
297+VAL MKCDATAc(VM* vm, CHeapItem * item) {
298+ c_heap_insert_if_needed(vm, &vm->c_heap, item);
299+ Closure* cl = allocate(sizeof(Closure), 1);
300+ SETTY(cl, CDATA);
301+ cl->info.c_heap_item = item;
302+ return cl;
303+}
304+
275VAL MKPTR(VM* vm, void* ptr) {
305VAL MKPTR(VM* vm, void* ptr) {
276 Closure* cl = allocate(sizeof(Closure), 0);
306 Closure* cl = allocate(sizeof(Closure), 0);
277 SETTY(cl, PTR);
307 SETTY(cl, PTR);
rts/idris_rts.h+40−5
@@ -27,7 +27,7 @@
27typedef enum {
27typedef enum {
28 CON, INT, BIGINT, FLOAT, STRING, STROFFSET,
28 CON, INT, BIGINT, FLOAT, STRING, STROFFSET,
29 BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD,
29 BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD,
30− MANAGEDPTR, RAWDATA
30+ MANAGEDPTR, RAWDATA, CDATA
31} ClosureType;
31} ClosureType;
32
32
33typedef struct Closure *VAL;
33typedef struct Closure *VAL;
@@ -67,20 +67,21 @@ typedef struct Closure {
67 uint32_t bits32;
67 uint32_t bits32;
68 uint64_t bits64;
68 uint64_t bits64;
69 ManagedPtr* mptr;
69 ManagedPtr* mptr;
70+ CHeapItem* c_heap_item;
70 size_t size;
71 size_t size;
71 } info;
72 } info;
72} Closure;
73} Closure;
73
74
74−struct VM_t;
75+struct VM;
75
76
76struct Msg_t {
77struct Msg_t {
77− struct VM_t* sender;
78+ struct VM* sender;
78 VAL msg;
79 VAL msg;
79};
80};
80
81
81typedef struct Msg_t Msg;
82typedef struct Msg_t Msg;
82
83
83−struct VM_t {
84+struct VM {
84 int active; // 0 if no longer running; keep for message passing
85 int active; // 0 if no longer running; keep for message passing
85 // TODO: If we're going to have lots of concurrent threads,
86 // TODO: If we're going to have lots of concurrent threads,
86 // we really need to be cleverer than this!
87 // we really need to be cleverer than this!
@@ -90,6 +91,7 @@ struct VM_t {
90 VAL* valstack_base;
91 VAL* valstack_base;
91 VAL* stack_max;
92 VAL* stack_max;
92
93
94+ CHeap c_heap;
93 Heap heap;
95 Heap heap;
94#ifdef HAS_PTHREAD
96#ifdef HAS_PTHREAD
95 pthread_mutex_t inbox_lock;
97 pthread_mutex_t inbox_lock;
@@ -110,7 +112,37 @@ struct VM_t {
110 VAL reg1;
112 VAL reg1;
111};
113};
112
114
113−typedef struct VM_t VM;
115+typedef struct VM VM;
116+
117+
118+/* C data interface: allocation on the C heap.
119+ *
120+ * Although not enforced in code, CData is meant to be opaque
121+ * and non-RTS code (such as libraries or C bindings) should
122+ * access only its (void *) field called "data".
123+ *
124+ * Feel free to mutate cd->data; the heap does not care
125+ * about its particular value. However, keep in mind
126+ * that it must not break Idris's referential transparency.
127+ *
128+ * If you call cdata_allocate or cdata_manage, the resulting
129+ * CData object *must* be returned from your FFI function so
130+ * that it is inserted in the C heap. Otherwise the memory
131+ * will be leaked.
132+ */
133+
134+/// C data block. Contains (void * data).
135+typedef CHeapItem * CData;
136+
137+/// Allocate memory, returning the corresponding C data block.
138+CData cdata_allocate(size_t size, CDataFinalizer * finalizer);
139+
140+/// Wrap a pointer as a C data block.
141+/// The size should be an estimate of how much memory, in bytes,
142+/// is associated with the pointer. This estimate need not be absolutely precise
143+/// but it is necessary for GC to work effectively.
144+CData cdata_manage(void * data, size_t size, CDataFinalizer * finalizer);
145+
114
146
115// Create a new VM
147// Create a new VM
116VM* init_vm(int stack_size, size_t heap_size,
148VM* init_vm(int stack_size, size_t heap_size,
@@ -150,6 +182,7 @@ typedef void(*func)(VM*, VAL*);
150#define GETPTR(x) (((VAL)(x))->info.ptr)
182#define GETPTR(x) (((VAL)(x))->info.ptr)
151#define GETMPTR(x) (((VAL)(x))->info.mptr->data)
183#define GETMPTR(x) (((VAL)(x))->info.mptr->data)
152#define GETFLOAT(x) (((VAL)(x))->info.f)
184#define GETFLOAT(x) (((VAL)(x))->info.f)
185+#define GETCDATA(x) (((VAL)(x))->info.c_heap_item)
153
186
154#define GETBITS8(x) (((VAL)(x))->info.bits8)
187#define GETBITS8(x) (((VAL)(x))->info.bits8)
155#define GETBITS16(x) (((VAL)(x))->info.bits16)
188#define GETBITS16(x) (((VAL)(x))->info.bits16)
@@ -210,6 +243,7 @@ VAL MKB8(VM* vm, uint8_t b);
210VAL MKB16(VM* vm, uint16_t b);
243VAL MKB16(VM* vm, uint16_t b);
211VAL MKB32(VM* vm, uint32_t b);
244VAL MKB32(VM* vm, uint32_t b);
212VAL MKB64(VM* vm, uint64_t b);
245VAL MKB64(VM* vm, uint64_t b);
246+VAL MKCDATA(VM* vm, CHeapItem * item);
213
247
214// following versions don't take a lock when allocating
248// following versions don't take a lock when allocating
215VAL MKFLOATc(VM* vm, double val);
249VAL MKFLOATc(VM* vm, double val);
@@ -217,6 +251,7 @@ VAL MKSTROFFc(VM* vm, StrOffset* off);
217VAL MKSTRc(VM* vm, char* str);
251VAL MKSTRc(VM* vm, char* str);
218VAL MKPTRc(VM* vm, void* ptr);
252VAL MKPTRc(VM* vm, void* ptr);
219VAL MKMPTRc(VM* vm, void* ptr, size_t size);
253VAL MKMPTRc(VM* vm, void* ptr, size_t size);
254+VAL MKCDATAc(VM* vm, CHeapItem * item);
220
255
221char* GETSTROFF(VAL stroff);
256char* GETSTROFF(VAL stroff);
222
257
src/IRTS/CodegenC.hs+3
@@ -354,6 +354,7 @@ toFType (FCon c)
354 | c == sUN "C_Float" = FArith ATFloat
354 | c == sUN "C_Float" = FArith ATFloat
355 | c == sUN "C_Ptr" = FPtr
355 | c == sUN "C_Ptr" = FPtr
356 | c == sUN "C_MPtr" = FManagedPtr
356 | c == sUN "C_MPtr" = FManagedPtr
357+ | c == sUN "C_CData" = FCData
357 | c == sUN "C_Unit" = FUnit
358 | c == sUN "C_Unit" = FUnit
358toFType (FApp c [_,ity])
359toFType (FApp c [_,ity])
359 | c == sUN "C_IntT" = FArith (toAType ity)
360 | c == sUN "C_IntT" = FArith (toAType ity)
@@ -378,6 +379,7 @@ c_irts FUnit l x = x
378c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"
379c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"
379c_irts FManagedPtr l x = l ++ "MKMPTR(vm, " ++ x ++ ")"
380c_irts FManagedPtr l x = l ++ "MKMPTR(vm, " ++ x ++ ")"
380c_irts (FArith ATFloat) l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"
381c_irts (FArith ATFloat) l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"
382+c_irts FCData l x = l ++ "MKCDATA(vm, " ++ x ++ ")"
381c_irts FAny l x = l ++ x
383c_irts FAny l x = l ++ x
382c_irts FFunction l x = error "Return of function from foreign call is not supported"
384c_irts FFunction l x = error "Return of function from foreign call is not supported"
383c_irts FFunctionIO l x = error "Return of function from foreign call is not supported"
385c_irts FFunctionIO l x = error "Return of function from foreign call is not supported"
@@ -391,6 +393,7 @@ irts_c FUnit x = x
391irts_c FPtr x = "GETPTR(" ++ x ++ ")"
393irts_c FPtr x = "GETPTR(" ++ x ++ ")"
392irts_c FManagedPtr x = "GETMPTR(" ++ x ++ ")"
394irts_c FManagedPtr x = "GETMPTR(" ++ x ++ ")"
393irts_c (FArith ATFloat) x = "GETFLOAT(" ++ x ++ ")"
395irts_c (FArith ATFloat) x = "GETFLOAT(" ++ x ++ ")"
396+irts_c FCData x = "GETCDATA(" ++ x ++ ")"
394irts_c FAny x = x
397irts_c FAny x = x
395irts_c FFunctionIO x = wrapped x
398irts_c FFunctionIO x = wrapped x
396irts_c FFunction x = wrapped x
399irts_c FFunction x = wrapped x
src/IRTS/Lang.hs+1
@@ -99,6 +99,7 @@ data FType = FArith ArithTy
99 | FUnit
99 | FUnit
100 | FPtr
100 | FPtr
101 | FManagedPtr
101 | FManagedPtr
102+ | FCData
102 | FAny
103 | FAny
103 deriving (Show, Eq)
104 deriving (Show, Eq)
104
105
test/Makefile+1−1
@@ -12,7 +12,7 @@ info: runtest
12 @./runtest $(patsubst %.test,%,$@) -q
12 @./runtest $(patsubst %.test,%,$@) -q
13
13
14test_js: runtest
14test_js: runtest
15− @./runtest without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 basic007 basic011 ffi006 ffi007 primitives005 opts --codegen node
15+ @./runtest without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 basic007 basic011 ffi006 ffi007 primitives005 primitives006 opts --codegen node
16
16
17update: runtest
17update: runtest
18 @./runtest all -u
18 @./runtest all -u
test/primitives006/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 export
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+export
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+export
27+bytesPerInt : Int
28+bytesPerInt = 8
29+
30+export
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+export
37+reallocate : Int -> ByteArray -> IO ()
38+reallocate newSz (BA ptr sz)
39+ = foreign FFI_C "array_realloc" (Int -> CData -> IO ()) sz ptr
40+
41+export
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+export
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+export
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+export
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+export
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+export
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+export
84+size : ByteArray -> Int
85+size (BA ptr sz) = sz
86+
87+export
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+export
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/primitives006/Data/Bytes.idrnew file+287
@@ -0,0 +1,287 @@
1+module Data.Bytes
2+
3+import Data.ByteArray as BA
4+
5+%access public export
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+export
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+export
36+length : Bytes -> Int
37+length (B arr ofs end) = end - ofs
38+
39+export
40+empty : Bytes
41+empty = unsafePerformIO $ allocate minimalCapacity
42+
43+export
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+export
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+export
85+(|>) : Bytes -> Byte -> Bytes
86+(|>) = snoc
87+
88+namespace SnocView
89+ data SnocView : Type where
90+ Nil : SnocView
91+ Snoc : (bs : Bytes) -> (b : Byte) -> SnocView
92+
93+ export
94+ snocView : Bytes -> SnocView
95+ snocView (B arr ofs end) =
96+ if end == ofs
97+ then SnocView.Nil
98+ else unsafePerformIO $ do
99+ last <- BA.peek (end-1) arr
100+ return $ SnocView.Snoc (B arr ofs (end-1)) last
101+
102+namespace ConsView
103+ data ConsView : Type where
104+ Nil : ConsView
105+ Cons : (b : Byte) -> (bs : Bytes) -> ConsView
106+
107+ export
108+ consView : Bytes -> ConsView
109+ consView (B arr ofs end) =
110+ if end == ofs
111+ then ConsView.Nil
112+ else unsafePerformIO $ do
113+ first <- BA.peek ofs arr
114+ return $ ConsView.Cons first (B arr (ofs+1) end)
115+
116+infixr 7 ++
117+%assert_total
118+export
119+(++) : Bytes -> Bytes -> Bytes
120+(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)
121+ = let countR = endR - ofsR in
122+ if endL + countR > BA.size arrL
123+ then unsafePerformIO $ do -- need more space
124+ grown <- grow 2 bsL
125+ return $ grown ++ bsR
126+ else unsafePerformIO $ do
127+ maxUsedL <- BA.peekInt 0 arrL
128+ if maxUsedL > endL
129+ then do -- headroom taken
130+ copyL <- grow 2 bsL
131+ return $ copyL ++ bsR
132+ else do -- can mutate
133+ BA.pokeInt 0 (endL + countR) arrL
134+ BA.copy (arrR, ofsR) (arrL, endL) countR
135+ return $ B arrL ofsL (endL + countR)
136+
137+export
138+dropPrefix : Int -> Bytes -> Bytes
139+dropPrefix n (B arr ofs end) = B arr (((ofs + n) `min` end) `max` dataOfs) end
140+
141+export
142+takePrefix : Int -> Bytes -> Bytes
143+takePrefix n (B arr ofs end) = B arr ofs (((ofs + n) `min` end) `max` dataOfs)
144+
145+export
146+pack : List Byte -> Bytes
147+pack = fromList empty
148+ where
149+ fromList : Bytes -> List Byte -> Bytes
150+ fromList bs [] = bs
151+ fromList bs (x :: xs) = fromList (bs `snoc` x) xs
152+
153+export
154+unpack : Bytes -> List Byte
155+unpack bs with (consView bs)
156+ | Nil = []
157+ | Cons x xs = x :: unpack (assert_smaller bs xs)
158+
159+export
160+slice : Int -> Int -> Bytes -> Bytes
161+slice ofs' end' (B arr ofs end)
162+ = B arr
163+ (((ofs + ofs') `min` end) `max` dataOfs)
164+ (((ofs + end') `min` end) `max` dataOfs)
165+
166+-- Folds with early exit.
167+-- If Bytes were a Functor, this would be equivalent
168+-- to a Traversable implementation interpreted in the Either monad.
169+data Result : Type -> Type where
170+ Stop : (result : a) -> Result a
171+ Cont : (acc : a) -> Result a
172+
173+export
174+iterateR : (Byte -> a -> Result a) -> a -> Bytes -> a
175+iterateR f acc bs with (snocView bs)
176+ | Nil = acc
177+ | Snoc ys y with (f y acc)
178+ | Stop result = result
179+ | Cont acc' = iterateR f acc' (assert_smaller bs ys)
180+
181+export
182+iterateL : (a -> Byte -> Result a) -> a -> Bytes -> a
183+iterateL f acc bs with (consView bs)
184+ | Nil = acc
185+ | Cons y ys with (f acc y)
186+ | Stop result = result
187+ | Cont acc' = iterateL f acc' (assert_smaller bs ys)
188+
189+infixl 3 .:
190+private
191+(.:) : (a -> b) -> (c -> d -> a) -> (c -> d -> b)
192+(.:) g f x y = g (f x y)
193+
194+export
195+foldr : (Byte -> a -> a) -> a -> Bytes -> a
196+foldr f = iterateR (Cont .: f)
197+
198+export
199+foldl : (a -> Byte -> a) -> a -> Bytes -> a
200+foldl f = iterateL (Cont .: f)
201+
202+export
203+spanLength : (Byte -> Bool) -> Bytes -> Int
204+spanLength p = iterateL step 0
205+ where
206+ step : Int -> Byte -> Result Int
207+ step n b with (p b)
208+ | True = Cont (1 + n)
209+ | False = Stop n
210+
211+find : Byte -> Bytes -> Maybe Int
212+find b (B arr ofs end) = unsafePerformIO $ BA.find b arr ofs end
213+
214+export
215+splitAt : Int -> Bytes -> (Bytes, Bytes)
216+splitAt n bs = (takePrefix n bs, dropPrefix n bs)
217+
218+export
219+splitOn : Byte -> Bytes -> (Bytes, Bytes)
220+splitOn b bs with (find b bs)
221+ | Nothing = (bs, empty)
222+ | Just ofs = (takePrefix ofs bs, dropPrefix (ofs+1) bs)
223+
224+export
225+splitsOn : Byte -> Bytes -> List Bytes
226+splitsOn b bs with (find b bs)
227+ | Nothing = [bs]
228+ | Just ofs = takePrefix ofs bs :: splitsOn b (assert_smaller bs $ dropPrefix (ofs+1) bs)
229+
230+export
231+asciiLines : Bytes -> List Bytes
232+asciiLines = splitsOn 0x0A
233+
234+export
235+span : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
236+span p bs = splitAt (spanLength p bs) bs
237+
238+export
239+break : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
240+break p bs = span (not . p) bs
241+
242+private
243+cmp : Bytes -> Bytes -> Ordering
244+cmp (B arrL ofsL endL) (B arrR ofsR endR) = unsafePerformIO $ do
245+ let countL = endL - ofsL
246+ let countR = endR - ofsR
247+ let commonCount = countL `min` countR
248+ result <- BA.compare (arrL, ofsL) (arrR, ofsR) commonCount
249+ return $
250+ if result /= 0
251+ then i2o result
252+ else compare countL countR
253+ where
254+ i2o : Int -> Ordering
255+ i2o 0 = EQ
256+ i2o i = if i < 0 then LT else GT
257+
258+implementation Eq Bytes where
259+ xs == ys = (Bytes.cmp xs ys == EQ)
260+
261+implementation Ord Bytes where
262+ compare = Bytes.cmp
263+
264+export
265+toString : Bytes -> String
266+toString = foldr (strCons . chr . toInt) ""
267+
268+export
269+fromString : String -> Bytes
270+fromString = foldl (\bs, c => bs |> fromInt (ord c)) empty . unpack
271+
272+implementation Show Bytes where
273+ show = ("b" ++) . show . toString
274+
275+implementation Semigroup Bytes where
276+ (<+>) = (++)
277+
278+implementation Monoid Bytes where
279+ neutral = empty
280+
281+-- todo:
282+--
283+-- make indices Nats
284+-- Build a ByteString on top of Bytes?
285+-- migrate to (Bits 8)?
286+--
287+-- bidirectional growth?
test/primitives006/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/primitives006/array.hnew file+18
@@ -0,0 +1,18 @@
1+#pragma once
2+
3+#include <stdint.h>
4+#include <stddef.h>
5+
6+#include "idris_rts.h"
7+
8+
9+CData array_alloc(int size);
10+void array_realloc(int size, CData array);
11+uint8_t array_peek(int ofs, CData array);
12+int array_peek_int(int ofs, CData array);
13+void array_poke(int ofs, uint8_t byte, CData array);
14+void array_poke_int(int ofs, int i, CData array);
15+void array_copy(CData src, int src_ofs, CData dst, int dst_ofs, int count);
16+void array_fill(int ofs, int count, uint8_t byte, CData array);
17+int array_compare(CData l, int lofs, CData r, int rofs, int count);
18+int array_find(uint8_t byte, CData array, int ofs, int end);
test/primitives006/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/primitives006/load-test.idrnew file+48
@@ -0,0 +1,48 @@
1+module Main
2+
3+import Data.Bytes as B
4+import Data.ByteArray as BA
5+
6+-- %flag C "-g3 -ggdb -O0"
7+%link C "array.o"
8+
9+initialBuf : Bytes
10+initialBuf = pack . concat $ replicate 128 block
11+ where
12+ block : List Byte
13+ 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]
14+
15+unRLE : Bytes -> Bytes
16+unRLE = fst . iterateL phi (empty, Nothing)
17+ where
18+ phi : (Bytes, Maybe Byte) -> Byte -> Result (Bytes, Maybe Byte)
19+ phi (bs, Nothing) b = Cont (bs, Just b)
20+ phi (bs, Just cnt) b = Cont (bs ++ pack (replicate (cast $ prim__zextB8_Int cnt) b), Nothing)
21+
22+unit : Int -> Byte -> IO ()
23+unit n b =
24+ let expanded = unRLE initialBuf
25+ in let elines = map (flip snoc b) (asciiLines expanded)
26+ in printLn $ (show b ++ "/" ++ show n, length expanded, length elines)
27+
28+alloc : Int -> Int -> IO Int
29+alloc x 0 = return x
30+alloc x i = do
31+ -- allocate an array
32+ arr <- BA.allocate (64 * 1024 * 1024)
33+ -- write "i" at offset 63M
34+ BA.pokeInt (63*1024*1024) i arr
35+ -- read number from offset 63M
36+ j <- BA.peekInt (63*1024*1024) arr
37+ -- count matches
38+ alloc (x + if i == j then 1 else 0) (i - 1)
39+
40+main : IO ()
41+main = do
42+ -- First allocate 1024 64M arrays to break the C heap if there's a bug
43+ alloc 0 1024 >>= printLn
44+
45+ -- Then, test Bytes
46+ traverse_ (unit n . prim__truncInt_B8) [1..n]
47+ where
48+ n = 8
test/primitives006/runnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env bash
2+${CC:-cc} -c -O2 -o array.o array.c $(${IDRIS:-idris} --include)
3+${IDRIS:-idris} $@ -o load-test load-test.idr --nocolour --warnreach
4+./load-test
5+rm -f load-test *.o *.ibc
6+find -name \*.ibc -delete