d4ffc21 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add ManagedPtr type

A ManagedPtr is just like a Ptr, except it points to memory inside Idris' heap, so doesn't need to be freed. This is useful when you need to create a structure C side for interacting with a C library, but don't want to have to explicitly free it. Also added registerPtr : (p : Ptr) -> (n : Int) -> ManagedPtr This moves the n bytes pointed to by p into the Idris heap. In a non-C backend, or one where memory is managed differently, it's entirely reasonable for this to be compiled as a no-op. The FFI treats both Ptr and ManagedPtr as a void* in C.

commitd4ffc21999a22c9433bd1bb11fcf3cadd0ce438f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 2 Mar 2014, 00:30 (13 years ago) parentbd744f1

13 files changed+69−3

compare with master

unifiedsplit

libs/prelude/IO.idr+8 rts/idris_gc.c+3 rts/idris_rts.c+25 rts/idris_rts.h+10−1 rts/idris_stdfgn.c+4 rts/idris_stdfgn.h+2 src/IRTS/CodegenC.hs+4 src/IRTS/Compiler.hs+1 src/IRTS/Lang.hs+2 src/Idris/Core/TT.hs+3−1 src/Idris/IBC.hs+2 src/Idris/ParseExpr.hs+2 src/Idris/Primitives.hs+3−1

libs/prelude/IO.idr+8

@@ -32,6 +32,7 @@ data FTy = FIntT IntTy

3232 | FFloat

3333 | FString

3434 | FPtr

35+ | FManagedPtr

3536 | FAny Type

3637 | FUnit

3738

@@ -85,6 +86,7 @@ interpFTy (FAny t) = t

8586interpFTy FFloat = Float

8687interpFTy FString = String

8788interpFTy FPtr = Ptr

89+interpFTy FManagedPtr = ManagedPtr

8890interpFTy (FIntT IT8x16) = Bits8x16

8991interpFTy (FIntT IT16x8) = Bits16x8

9092interpFTy (FIntT IT32x4) = Bits32x4

@@ -106,6 +108,9 @@ mkForeignPrim : Foreign x -> x

106108mkLazyForeignPrim : Foreign x -> x

107109-- mkForeign and mkLazyForeign compiled as primitives

108110

111+registerPtr : Ptr -> Int -> ManagedPtr

112+registerPtr = prim__registerPtr

113+

109114abstract

110115io_bind : IO a -> (a -> IO b) -> IO b

111116io_bind (MkIO fn) k

@@ -149,3 +154,6 @@ unsafePerformIO (MkIO f) = unsafePerformPrimIO

149154 (prim_io_bind (f TheWorld) (\ b => prim_io_return b))

150155

151156

157+forceGC : IO ()

158+forceGC = mkForeign (FFun "idris_forceGC" [FPtr] FUnit) prim__vm

159+

rts/idris_gc.c+3

@@ -36,6 +36,9 @@ VAL copy(VM* vm, VAL x) {

3636 case PTR:

3737 cl = MKPTRc(vm, x->info.ptr);

3838 break;

39+ case MANAGEDPTR:

40+ cl = MKMPTRc(vm, x->info.mptr->data, x->info.mptr->size);

41+ break;

3942 case BITS8:

4043 cl = idris_b8CopyForGC(vm, x);

4144 break;

rts/idris_rts.c+25

@@ -178,6 +178,17 @@ VAL MKPTR(VM* vm, void* ptr) {

178178 return cl;

179179}

180180

181+VAL MKMPTR(VM* vm, void* ptr, int size) {

182+ Closure* cl = allocate(vm, sizeof(Closure) +

183+ sizeof(ManagedPtr) + size, 0);

184+ SETTY(cl, MANAGEDPTR);

185+ cl->info.mptr = (ManagedPtr*)((char*)cl + sizeof(Closure));

186+ cl->info.mptr->data = (char*)cl + sizeof(Closure) + sizeof(ManagedPtr);

187+ memcpy(cl->info.mptr->data, ptr, size);

188+ cl->info.mptr->size = size;

189+ return cl;

190+}

191+

181192VAL MKFLOATc(VM* vm, double val) {

182193 Closure* cl = allocate(vm, sizeof(Closure), 1);

183194 SETTY(cl, FLOAT);

@@ -202,6 +213,17 @@ VAL MKPTRc(VM* vm, void* ptr) {

202213 return cl;

203214}

204215

216+VAL MKMPTRc(VM* vm, void* ptr, int size) {

217+ Closure* cl = allocate(vm, sizeof(Closure) +

218+ sizeof(ManagedPtr) + size, 1);

219+ SETTY(cl, MANAGEDPTR);

220+ cl->info.mptr = (ManagedPtr*)((char*)cl + sizeof(Closure));

221+ cl->info.mptr->data = (char*)cl + sizeof(Closure) + sizeof(ManagedPtr);

222+ memcpy(cl->info.mptr->data, ptr, size);

223+ cl->info.mptr->size = size;

224+ return cl;

225+}

226+

205227VAL MKB8(VM* vm, uint8_t bits8) {

206228 Closure* cl = allocate(vm, sizeof(Closure), 1);

207229 SETTY(cl, BITS8);

@@ -795,6 +817,9 @@ VAL copyTo(VM* vm, VAL x) {

795817 case PTR:

796818 cl = MKPTRc(vm, x->info.ptr);

797819 break;

820+ case MANAGEDPTR:

821+ cl = MKMPTRc(vm, x->info.mptr->data, x->info.mptr->size);

822+ break;

798823 case BITS8:

799824 cl = idris_b8CopyForGC(vm, x);

800825 break;

rts/idris_rts.h+10−1

@@ -17,7 +17,7 @@

1717typedef enum {

1818 CON, INT, BIGINT, FLOAT, STRING, STROFFSET,

1919 BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD,

20− BUFFER

20+ MANAGEDPTR, BUFFER

2121} ClosureType;

2222

2323typedef struct Closure *VAL;

@@ -40,6 +40,11 @@ typedef struct {

4040 unsigned char store[];

4141} Buffer;

4242

43+// A foreign pointer, managed by the idris GC

44+typedef struct {

45+ size_t size;

46+ void* data;

47+} ManagedPtr;

4348

4449typedef struct Closure {

4550// Use top 16 bits of ty for saying which heap value is in

@@ -57,6 +62,7 @@ typedef struct Closure {

5762 uint32_t bits32;

5863 uint64_t bits64;

5964 Buffer* buf;

65+ ManagedPtr* mptr;

6066 } info;

6167} Closure;

6268

@@ -112,6 +118,7 @@ typedef void(*func)(VM*, VAL*);

112118

113119#define GETSTR(x) (ISSTR(x) ? (((VAL)(x))->info.str) : GETSTROFF(x))

114120#define GETPTR(x) (((VAL)(x))->info.ptr)

121+#define GETMPTR(x) (((VAL)(x))->info.mptr->data)

115122#define GETFLOAT(x) (((VAL)(x))->info.f)

116123

117124#define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( (x)->ty == CON ? (x)->info.c.tag_arity >> 8 : (-1)) )

@@ -163,6 +170,7 @@ typedef intptr_t i_int;

163170VAL MKFLOAT(VM* vm, double val);

164171VAL MKSTR(VM* vm, const char* str);

165172VAL MKPTR(VM* vm, void* ptr);

173+VAL MKMPTR(VM* vm, void* ptr, int size);

166174VAL MKB8(VM* vm, uint8_t b);

167175VAL MKB16(VM* vm, uint16_t b);

168176VAL MKB32(VM* vm, uint32_t b);

@@ -173,6 +181,7 @@ VAL MKFLOATc(VM* vm, double val);

173181VAL MKSTROFFc(VM* vm, StrOffset* off);

174182VAL MKSTRc(VM* vm, char* str);

175183VAL MKPTRc(VM* vm, void* ptr);

184+VAL MKMPTRc(VM* vm, void* ptr, int size);

176185VAL MKBUFFERc(VM* vm, Buffer* buf);

177186

178187char* GETSTROFF(VAL stroff);

rts/idris_stdfgn.c+4

@@ -1,5 +1,6 @@

11#include "idris_stdfgn.h"

22#include "idris_rts.h"

3+#include "idris_gc.h"

34#include <sys/select.h>

45#include <fcntl.h>

56#include <stdio.h>

@@ -80,3 +81,6 @@ int idris_time() {

8081 return (int)t;

8182}

8283

84+void idris_forceGC(void* vm) {

85+ idris_gc((VM*)vm);

86+}

rts/idris_stdfgn.h+2

@@ -23,4 +23,6 @@ char* getEnvPair(int i);

2323

2424int idris_time();

2525

26+void idris_forceGC();

27+

2628#endif

src/IRTS/CodegenC.hs+4

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

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

263263c_irts FUnit l x = x

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

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

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

266267c_irts FAny l x = l ++ x

267268

@@ -272,6 +273,7 @@ irts_c (FArith (ATInt (ITFixed ity))) x

272273irts_c FString x = "GETSTR(" ++ x ++ ")"

273274irts_c FUnit x = x

274275irts_c FPtr x = "GETPTR(" ++ x ++ ")"

276+irts_c FManagedPtr x = "GETMPTR(" ++ x ++ ")"

275277irts_c (FArith ATFloat) x = "GETFLOAT(" ++ x ++ ")"

276278irts_c FAny x = x

277279

@@ -470,6 +472,8 @@ doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (sMN 0 "EVAL") ++ ",

470472doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

471473doOp v LVMPtr [] = v ++ "MKPTR(vm, vm)"

472474doOp v LNullPtr [] = v ++ "MKPTR(vm, NULL)"

475+doOp v LRegisterPtr [p, i] = v ++ "MKMPTR(vm, GETPTR(" ++ creg p ++

476+ "), GETINT(" ++ creg i ++ "))"

473477doOp v (LChInt ITNative) args = v ++ creg (last args)

474478doOp v (LChInt ITChar) args = doOp v (LChInt ITNative) args

475479doOp v (LIntCh ITNative) args = v ++ creg (last args)

src/IRTS/Compiler.hs+1

@@ -349,6 +349,7 @@ mkIty "FBits32" = mkIntIty "IT32"

349349mkIty "FBits64" = mkIntIty "IT64"

350350mkIty "FString" = FString

351351mkIty "FPtr" = FPtr

352+mkIty "FManagedPtr" = FManagedPtr

352353mkIty "FUnit" = FUnit

353354mkIty "FFunction" = FFunction

354355mkIty "FFunctionIO" = FFunctionIO

src/IRTS/Lang.hs+2

@@ -66,6 +66,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

6666 -- core or another machine. 'id' is a valid implementation

6767 | LVMPtr

6868 | LNullPtr

69+ | LRegisterPtr

6970 | LNoOp

7071 deriving (Show, Eq)

7172

@@ -83,6 +84,7 @@ data FType = FArith ArithTy

8384 | FString

8485 | FUnit

8586 | FPtr

87+ | FManagedPtr

8688 | FAny

8789 deriving (Show, Eq)

8890

src/Idris/Core/TT.hs+3−1

@@ -475,7 +475,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

475475 | B8V (Vector Word8) | B16V (Vector Word16)

476476 | B32V (Vector Word32) | B64V (Vector Word64)

477477 | AType ArithTy | StrType

478− | PtrType | BufferType | VoidType | Forgot

479479 deriving (Eq, Ord)

480480{-!

481481deriving instance Binary Const

@@ -495,6 +495,7 @@ instance Pretty Const OutputAnnotation where

495495 pretty StrType = text "String"

496496 pretty BufferType = text "prim__UnsafeBuffer"

497497 pretty PtrType = text "Ptr"

498+ pretty ManagedPtrType = text "Ptr"

498499 pretty VoidType = text "Void"

499500 pretty Forgot = text "Forgot"

500501 pretty (B8 w) = text . show $ w

@@ -1041,6 +1042,7 @@ instance Show Const where

10411042 show StrType = "String"

10421043 show BufferType = "prim__UnsafeBuffer"

10431044 show PtrType = "Ptr"

1045+ show ManagedPtrType = "ManagedPtr"

10441046 show VoidType = "Void"

10451047

10461048showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String

src/Idris/IBC.hs+2

@@ -617,6 +617,7 @@ instance Binary Const where

617617 B32V x1 -> putWord8 23 >> put x1

618618 B64V x1 -> putWord8 24 >> put x1

619619 BufferType -> putWord8 25

620+ ManagedPtrType -> putWord8 26

620621 get

621622 = do i <- getWord8

622623 case i of

@@ -658,6 +659,7 @@ instance Binary Const where

658659 23 -> fmap B32V get

659660 24 -> fmap B64V get

660661 25 -> return BufferType

662+ 26 -> return ManagedPtrType

661663

662664 _ -> error "Corrupted binary data for Const"

663665

src/Idris/ParseExpr.hs+2

@@ -1003,6 +1003,7 @@ Constant ::=

10031003 | 'Float'

10041004 | 'String'

10051005 | 'Ptr'

1006+ | 'ManagedPtr'

10061007 | 'prim__UnsafeBuffer'

10071008 | 'Bits8'

10081009 | 'Bits16'

@@ -1027,6 +1028,7 @@ constant = do reserved "Integer"; return (AType (ATInt ITBig))

10271028 <|> do reserved "Float"; return (AType ATFloat)

10281029 <|> do reserved "String"; return StrType

10291030 <|> do reserved "Ptr"; return PtrType

1031+ <|> do reserved "ManagedPtr"; return ManagedPtrType

10301032 <|> do reserved "prim__UnsafeBuffer"; return BufferType

10311033 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))

10321034 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))

src/Idris/Primitives.hs+3−1

@@ -172,7 +172,9 @@ primitives =

172172 (0, LStdIn) partial,

173173 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

174174 (0, LNullPtr) total,

175−

175+ -- Managed pointer registration

176+ Prim (sUN "prim__registerPtr") (ty [PtrType, AType (ATInt ITNative)] ManagedPtrType) 2 (p_cantreduce)

177+ (2, LRegisterPtr) total,

176178 -- Buffers

177179 Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_cantreduce)

178180 (1, LAllocate) total,