git.iko.soy/Idris-dev
on master help sign in
Add some buffer primitives
commit9c8b3d4eb559be118d7deb247f869e23ec24dc6a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 29 Dec 2017, 18:44 (9 years ago) parent4162113
7 files changed+123−3
compare with master
unifiedsplit
libs/base/Data/Buffer.idr+34−2 rts/idris_buffer.c+42 rts/idris_buffer.h+4 test/TestData.hs+2−1 test/buffer002/buffer002.idr+27 test/buffer002/expected+10 test/buffer002/run+4
libs/base/Data/Buffer.idr+34−2
@@ -2,7 +2,11 @@ module Data.Buffer
22
33%include C "idris_buffer.h"
44
5−||| A buffer is a pointer to a sized, unstructured, mutable chunk of memory
5+||| A buffer is a pointer to a sized, unstructured, mutable chunk of memory.
6+||| There are primitive operations for gettng and setting bytes, ints (32 bit)
7+||| and strings at a location in the buffer. These operations silently fail
8+||| if the location is out of bounds, so bounds checking should be done in
9+||| advance.
610export
711record Buffer where
812 constructor MkBuffer
@@ -47,6 +51,15 @@ setByte b loc val
4751 = foreign FFI_C "idris_setBufferByte" (ManagedPtr -> Int -> Bits8 -> IO ())
4852 (rawdata b) loc val
4953
54+||| Set the int at position 'loc' to 'val'.
55+||| Uses 4 bytes (assumes up to 32 bit Int).
56+||| Does nothing if the location is outside the bounds of the buffer
57+export
58+setInt : Buffer -> (loc : Int) -> (val : Int) -> IO ()
59+setInt b loc val
60+ = foreign FFI_C "idris_setBufferInt" (ManagedPtr -> Int -> Int -> IO ())
61+ (rawdata b) loc val
62+
5063||| Set the byte at position 'loc' to 'val'.
5164||| Does nothing if the location is out of bounds of the buffer, or the string
5265||| is too long for the location
@@ -66,13 +79,32 @@ copyData src start len dest loc
6679 = foreign FFI_C "idris_copyBuffer" (ManagedPtr -> Int -> Int -> ManagedPtr -> Int -> IO ())
6780 (rawdata src) start len (rawdata dest) loc
6881
69−||| Return the value at the given location in the buffer
82+||| Return the value at the given location in the buffer.
83+||| Returns 0 if out of bounds.
7084export
7185getByte : Buffer -> (loc : Int) -> IO Bits8
7286getByte b loc
7387 = foreign FFI_C "idris_getBufferByte" (ManagedPtr -> Int -> IO Bits8)
7488 (rawdata b) loc
7589
90+||| Return the value at the given location in the buffer, assuming 4
91+||| bytes to store the Int.
92+||| Returns 0 if out of bounds.
93+export
94+getInt : Buffer -> (loc : Int) -> IO Int
95+getInt b loc
96+ = foreign FFI_C "idris_getBufferInt" (ManagedPtr -> Int -> IO Int)
97+ (rawdata b) loc
98+
99+||| Return the string at the given location in the buffer, with the given
100+||| length. Returns "" if out of bounds.
101+export
102+getString : Buffer -> (loc : Int) -> (len : Int) -> IO String
103+getString b loc len
104+ = do MkRaw str <- foreign FFI_C "idris_getBufferString" (ManagedPtr -> Int -> Int -> IO (Raw String))
105+ (rawdata b) loc len
106+ pure str
107+
76108||| Read 'maxbytes' into the buffer from a file, returning a new
77109||| buffer with the 'locaton' pointer moved along
78110export
rts/idris_buffer.c+42
@@ -39,6 +39,16 @@ void idris_setBufferByte(void* buffer, int loc, uint8_t byte) {
3939 }
4040}
4141
42+void idris_setBufferInt(void* buffer, int loc, int val) {
43+ Buffer* b = buffer;
44+ if (loc >= 0 && loc+3 < b->size) {
45+ b->data[loc] = val & 0xff;
46+ b->data[loc+1] = (val >> 8) & 0xff;
47+ b->data[loc+2] = (val >> 16) & 0xff;
48+ b->data[loc+3] = (val >> 24) & 0xff;
49+ }
50+}
51+
4252void idris_setBufferString(void* buffer, int loc, char* str) {
4353 Buffer* b = buffer;
4454 int len = strlen(str);
@@ -57,6 +67,38 @@ uint8_t idris_getBufferByte(void* buffer, int loc) {
5767 }
5868}
5969
70+int idris_getBufferInt(void* buffer, int loc) {
71+ Buffer* b = buffer;
72+ if (loc >= 0 && loc+3 < b->size) {
73+ return b->data[loc] +
74+ (b->data[loc+1] << 8) +
75+ (b->data[loc+2] << 16) +
76+ (b->data[loc+3] << 24);
77+ } else {
78+ return 0;
79+ }
80+}
81+
82+VAL idris_getBufferString(void* buffer, int loc, int len) {
83+ Buffer* b = buffer;
84+
85+ Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
86+ sizeof(char)*(len+1), 0);
87+ SETTY(cl, CT_STRING);
88+ cl->info.str.str = (char*)cl + sizeof(Closure);
89+
90+ if (loc >= 0 && loc+len < b->size) {
91+ memcpy(cl->info.str.str, (b->data)+loc, len);
92+ cl->info.str.str[len]='\0';
93+ cl->info.str.len = len;
94+ } else {
95+ cl->info.str.str[0] = '\0';
96+ cl->info.str.len = 0;
97+ }
98+
99+ return cl;
100+}
101+
60102int idris_readBuffer(FILE* h, void* buffer, int loc, int max) {
61103 Buffer* b = buffer;
62104 size_t len;
rts/idris_buffer.h+4
@@ -4,12 +4,14 @@
44#include <stdlib.h>
55#include <stdio.h>
66#include <stdint.h>
7+#include "idris_rts.h"
78
89void* idris_newBuffer(int bytes);
910
1011int idris_getBufferSize(void* buffer);
1112
1213void idris_setBufferByte(void* buffer, int loc, uint8_t byte);
14+void idris_setBufferInt(void* buffer, int loc, int byte);
1315void idris_setBufferString(void* buffer, int loc, char* str);
1416
1517void idris_copyBuffer(void* from, int start, int len,
@@ -19,5 +21,7 @@ int idris_readBuffer(FILE* h, void* buffer, int loc, int max);
1921void idris_writeBuffer(FILE* h, void* buffer, int loc, int len);
2022
2123uint8_t idris_getBufferByte(void* buffer, int loc);
24+int idris_getBufferInt(void* buffer, int loc);
25+VAL idris_getBufferString(void* buffer, int loc, int len);
2226
2327#endif
test/TestData.hs+2−1
@@ -83,7 +83,8 @@ testFamiliesData = [
8383 ("bounded", "Bounded",
8484 [ ( 1, ANY )]),
8585 ("buffer", "Buffer",
86− [ ( 1, C_CG )]),
86+ [ ( 1, C_CG ),
87+ ( 2, C_CG )]),
8788 ("contrib", "Contrib",
8889 [ ( 1, C_CG )]),
8990 ("corecords", "Corecords",
test/buffer002/buffer002.idrnew file+27
@@ -0,0 +1,27 @@
1+import Data.Buffer
2+
3+main : IO ()
4+main = do Just buf <- newBuffer 40
5+ printLn (size buf)
6+ setInt buf 5 1234567890
7+ setInt buf 36 1234567890
8+ setString buf 20 "Hello world!"
9+ printLn !(bufferData buf)
10+
11+ val <- getInt buf 5
12+ printLn val
13+ val <- getInt buf 6
14+ printLn val
15+ val <- getInt buf 36
16+ printLn val
17+ val <- getInt buf 37 -- out of bounds, expect 0
18+ printLn val
19+
20+ str <- getString buf 20 10
21+ putStrLn str
22+ str <- getString buf 20 12
23+ putStrLn str
24+ str <- getString buf 200 12 -- out of bounds, expect ""
25+ printLn str
26+ str <- getString buf 35 12 -- out of bounds, expect ""
27+ printLn str
test/buffer002/expectednew file+10
@@ -0,0 +1,10 @@
1+40
2+[00, 00, 00, 00, 00, D2, 02, 96, 49, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 48, 65, 6C, 6C, 6F, 20, 77, 6F, 72, 6C, 64, 21, 00, 00, 00, 00, D2, 02, 96, 49]
3+1234567890
4+4822530
5+1234567890
6+0
7+Hello worl
8+Hello world!
9+""
10+""
test/buffer002/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ buffer002.idr -o buffer002
3+./buffer002
4+rm -f buffer002 test.buf *.ibc