9c8b3d4 · Idris-dev · git.iko.soy

libs/base/Data/Buffer.idr+34−2

compare with master

unifiedsplit

@@ -2,7 +2,11 @@ module Data.Buffer

2

3%include C "idris_buffer.h"

4

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.

6export

10export

7record Buffer where

11record Buffer where

8 constructor MkBuffer

12 constructor MkBuffer

@@ -47,6 +51,15 @@ setByte b loc val

47 = foreign FFI_C "idris_setBufferByte" (ManagedPtr -> Int -> Bits8 -> IO ())

51 = foreign FFI_C "idris_setBufferByte" (ManagedPtr -> Int -> Bits8 -> IO ())

48 (rawdata b) loc val

52 (rawdata b) loc val

49

53

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+

50||| Set the byte at position 'loc' to 'val'.

63||| Set the byte at position 'loc' to 'val'.

51||| Does nothing if the location is out of bounds of the buffer, or the string

64||| Does nothing if the location is out of bounds of the buffer, or the string

52||| is too long for the location

65||| is too long for the location

@@ -66,13 +79,32 @@ copyData src start len dest loc

66 = foreign FFI_C "idris_copyBuffer" (ManagedPtr -> Int -> Int -> ManagedPtr -> Int -> IO ())

79 = foreign FFI_C "idris_copyBuffer" (ManagedPtr -> Int -> Int -> ManagedPtr -> Int -> IO ())

67 (rawdata src) start len (rawdata dest) loc

80 (rawdata src) start len (rawdata dest) loc

68

81

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.

70export

84export

71getByte : Buffer -> (loc : Int) -> IO Bits8

85getByte : Buffer -> (loc : Int) -> IO Bits8

72getByte b loc

86getByte b loc

73 = foreign FFI_C "idris_getBufferByte" (ManagedPtr -> Int -> IO Bits8)

87 = foreign FFI_C "idris_getBufferByte" (ManagedPtr -> Int -> IO Bits8)

74 (rawdata b) loc

88 (rawdata b) loc

75

89

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+

76||| Read 'maxbytes' into the buffer from a file, returning a new

108||| Read 'maxbytes' into the buffer from a file, returning a new

77||| buffer with the 'locaton' pointer moved along

109||| buffer with the 'locaton' pointer moved along

78export

110export

rts/idris_buffer.c+42

@@ -39,6 +39,16 @@ void idris_setBufferByte(void* buffer, int loc, uint8_t byte) {

39 }

40}

41

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+

42void idris_setBufferString(void* buffer, int loc, char* str) {

52void idris_setBufferString(void* buffer, int loc, char* str) {

43 Buffer* b = buffer;

53 Buffer* b = buffer;

44 int len = strlen(str);

54 int len = strlen(str);

@@ -57,6 +67,38 @@ uint8_t idris_getBufferByte(void* buffer, int loc) {

57 }

67 }

58}

68}

59

69

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+

60int idris_readBuffer(FILE* h, void* buffer, int loc, int max) {

102int idris_readBuffer(FILE* h, void* buffer, int loc, int max) {

61 Buffer* b = buffer;

103 Buffer* b = buffer;

62 size_t len;

104 size_t len;

rts/idris_buffer.h+4

@@ -4,12 +4,14 @@

4#include <stdlib.h>

5#include <stdio.h>

6#include <stdint.h>

7+#include "idris_rts.h"

7

8

8void* idris_newBuffer(int bytes);

9void* idris_newBuffer(int bytes);

9

10

10int idris_getBufferSize(void* buffer);

11int idris_getBufferSize(void* buffer);

11

12

12void idris_setBufferByte(void* buffer, int loc, uint8_t byte);

13void idris_setBufferByte(void* buffer, int loc, uint8_t byte);

14+void idris_setBufferInt(void* buffer, int loc, int byte);

13void idris_setBufferString(void* buffer, int loc, char* str);

15void idris_setBufferString(void* buffer, int loc, char* str);

14

16

15void idris_copyBuffer(void* from, int start, int len,

17void idris_copyBuffer(void* from, int start, int len,

@@ -19,5 +21,7 @@ int idris_readBuffer(FILE* h, void* buffer, int loc, int max);

19void idris_writeBuffer(FILE* h, void* buffer, int loc, int len);

21void idris_writeBuffer(FILE* h, void* buffer, int loc, int len);

20

22

21uint8_t idris_getBufferByte(void* buffer, int loc);

23uint8_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);

22

26

23#endif

27#endif

test/TestData.hs+2−1

@@ -83,7 +83,8 @@ testFamiliesData = [

83 ("bounded", "Bounded",

84 [ ( 1, ANY )]),

85 ("buffer", "Buffer",

86− [ ( 1, C_CG )]),

86+ [ ( 1, C_CG ),

87+ ( 2, C_CG )]),

87 ("contrib", "Contrib",

88 ("contrib", "Contrib",

88 [ ( 1, C_CG )]),

89 [ ( 1, C_CG )]),

89 ("corecords", "Corecords",

90 ("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