713e485 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

newBuffer should return a managed pointer

Otherwise, we're just guessing on the size, and that way lies segfaults. It turns out the size in Buffer.idr might have been correct once, but isn't now, and so unless we're lucky registering the pointer will copy memory we don't have access to. If the RTS does the registering of the pointer, at least it knows the size. (It's likely this is doable without the malloc, using iallocate directly, but this required fewer changes.)

commit713e485ff6d35f11b1e29b20388d02ff5c43d0db authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 30 Jul 2018, 16:54 (8 years ago) parentf70d4fa

6 files changed+24−9

compare with master

unifiedsplit

libs/base/Data/Buffer.idr+5−4 libs/prelude/Builtins.idr+1 libs/prelude/Prelude/Strings.idr+8 rts/idris_buffer.c+7−3 rts/idris_buffer.h+1−1 src/IRTS/CodegenC.hs+2−1

libs/base/Data/Buffer.idr+5−4

@@ -21,11 +21,12 @@ record Buffer where

2121||| fails

2222export

2323newBuffer : (size : Int) -> IO (Maybe Buffer)

24−newBuffer size = do bptr <- foreign FFI_C "idris_newBuffer" (Int -> IO Ptr)

25− size

26− bad <- nullPtr bptr

24+newBuffer size = do vm <- getMyVM

25+ bptr <- foreign FFI_C "idris_newBuffer" (Ptr -> Int -> IO ManagedPtr)

26+ vm size

27+ bad <- nullManagedPtr bptr

2728 if bad then pure Nothing

28− else pure (Just (MkBuffer (prim__registerPtr bptr (size + 8)) size 0))

29+ else pure (Just (MkBuffer bptr size 0))

2930

3031||| Reset the 'next location' pointer of the buffer to 0.

3132||| The 'next location' pointer gives the location for the next file read/write

libs/prelude/Builtins.idr+1

@@ -206,6 +206,7 @@ export data CData : Type

206206%extern prim__stderr : Ptr

207207

208208%extern prim__null : Ptr

209+%extern prim__managedNull : ManagedPtr

209210%extern prim__eqPtr : Ptr -> Ptr -> Int

210211%extern prim__eqManagedPtr : ManagedPtr -> ManagedPtr -> Int

211212%extern prim__registerPtr : Ptr -> Int -> ManagedPtr

libs/prelude/Prelude/Strings.idr+8

@@ -146,6 +146,9 @@ reverse = prim__strRev

146146null : Ptr

147147null = prim__null

148148

149+managedNull : ManagedPtr

150+managedNull = prim__managedNull

151+

149152-- Some more complex string operations

150153

151154data StrM : String -> Type where

@@ -398,6 +401,11 @@ nullPtr : Ptr -> IO Bool

398401nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p

399402 pure (ok /= 0)

400403

404+partial

405+nullManagedPtr : ManagedPtr -> IO Bool

406+nullManagedPtr p = do ok <- foreign FFI_C "isNull" (ManagedPtr -> IO Int) p

407+ pure (ok /= 0)

408+

401409||| Check if a supposed string was actually a null pointer

402410partial

403411nullStr : String -> IO Bool

rts/idris_buffer.c+7−3

@@ -6,8 +6,10 @@ typedef struct {

66 uint8_t data[0];

77} Buffer;

9−void* idris_newBuffer(int bytes) {

10− Buffer* buf = malloc(sizeof(Buffer) + bytes*sizeof(uint8_t));

9+VAL idris_newBuffer(VM* vm, int bytes) {

10+ size_t size = sizeof(Buffer) + bytes*sizeof(uint8_t);

11+

12+ Buffer* buf = malloc(size);

1113 if (buf == NULL) {

1214 return NULL;

1315 }

@@ -15,7 +17,9 @@ void* idris_newBuffer(int bytes) {

1517 buf->size = bytes;

1618 memset(buf->data, 0, bytes);

1719

18− return buf;

20+ void* retbuf = MKMPTR(vm, buf, size);

21+ free(buf);

22+ return retbuf;

1923}

2024

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

rts/idris_buffer.h+1−1

@@ -6,7 +6,7 @@

66#include <stdint.h>

77#include "idris_rts.h"

9−void* idris_newBuffer(int bytes);

9+VAL idris_newBuffer(VM* vm, int bytes);

1010

1111int idris_getBufferSize(void* buffer);

1212

src/IRTS/CodegenC.hs+2−1

@@ -389,7 +389,7 @@ c_irts (FArith (ATInt (ITFixed ity))) l x

389389c_irts FString l x = l ++ "MKSTR(vm, " ++ x ++ ")"

390390c_irts FUnit l x = x

391391c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"

392−c_irts FManagedPtr l x = l ++ "MKMPTR(vm, " ++ x ++ ")"

392+c_irts FManagedPtr l x = l ++ x

393393c_irts (FArith ATFloat) l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"

394394c_irts FCData l x = l ++ "MKCDATA(vm, " ++ x ++ ")"

395395c_irts FAny l x = l ++ x

@@ -644,6 +644,7 @@ doOp v (LExternal se) [] | se == sUN "prim__stderr" = v ++ "MKPTR(vm, stderr)"

644644

645645doOp v (LExternal vm) [_] | vm == sUN "prim__vm" = v ++ "MKPTR(vm, vm)"

646646doOp v (LExternal nul) [] | nul == sUN "prim__null" = v ++ "MKPTR(vm, NULL)"

647+doOp v (LExternal nul) [] | nul == sUN "prim__managedNull" = v ++ "MKPTR(vm, NULL)"

647648doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqPtr"

648649 = v ++ "MKINT((i_int)(GETPTR(" ++ creg x ++ ") == GETPTR(" ++ creg y ++ ")))"

649650doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqManagedPtr"