e294e0e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Proper initialization semantics for raw memory

commite294e0e1cbf1a9c0364c6c8225885b15cb3d2cfc authorJan Bessai <Jan.Bessai@tu-dortmund.de> dateFri 5 Apr 2013, 15:40 (14 years ago) parentb6effdb

7 files changed+134−53

compare with master

unifiedsplit

effects/Effect/Memory.idr+76−48 java/src/main/java/org/idris/rts/ForeignPrimitives.java+10 rts/idris_rts.c+32 rts/idris_rts.h+5 src/IRTS/CodegenC.hs+4 src/IRTS/CodegenJava.hs+4−3 test/test025/test025.idr+3−2

effects/Effect/Memory.idr+76−48

@@ -6,30 +6,35 @@ import Control.IOExcept

66%access public

88abstract

9−data MemoryChunk : Nat -> Type where

10− CH : Ptr -> (size : Nat) -> MemoryChunk size

9+data MemoryChunk : Nat -> Nat -> Type where

10+ CH : Ptr -> MemoryChunk size initialized

1111

1212abstract

1313data RawMemory : Effect where

14− Allocate : (n : Nat) ->

15− RawMemory () (MemoryChunk n) ()

16− Free : RawMemory (MemoryChunk n) () ()

17− Peek : (offset : Nat) ->

18− (size : Nat) ->

19− so (offset + size <= n) ->

20− RawMemory (MemoryChunk n) (MemoryChunk n) (Vect Bits8 size)

21− Poke : (offset : Nat) ->

22− (Vect Bits8 size) ->

23− so (offset + size <= n) ->

24− RawMemory (MemoryChunk n) (MemoryChunk n) ()

25− Move : (src : MemoryChunk m) ->

26− (dest_offset : Nat) ->

27− (src_offset : Nat) ->

28− (size : Nat) ->

29− so (dest_offset + size <= n) ->

30− so (src_offset + size <= m) ->

31− RawMemory (MemoryChunk n) (MemoryChunk n) ()

32− GetRawPtr : RawMemory (MemoryChunk n) (MemoryChunk n) (MemoryChunk n)

14+ Allocate : (n : Nat) ->

15+ RawMemory () (MemoryChunk n 0) ()

16+ Free : RawMemory (MemoryChunk n i) () ()

17+ Initialize : Bits8 ->

18+ (size : Nat) ->

19+ so (i + size <= n) ->

20+ RawMemory (MemoryChunk n i) (MemoryChunk n (i + size)) ()

21+ Peek : (offset : Nat) ->

22+ (size : Nat) ->

23+ so (offset + size <= i) ->

24+ RawMemory (MemoryChunk n i) (MemoryChunk n i) (Vect Bits8 size)

25+ Poke : (offset : Nat) ->

26+ (Vect Bits8 size) ->

27+ so (offset <= i && offset + size <= n) ->

28+ RawMemory (MemoryChunk n i) (MemoryChunk n (max i (offset + size))) ()

29+ Move : (src : MemoryChunk src_size src_init) ->

30+ (dst_offset : Nat) ->

31+ (src_offset : Nat) ->

32+ (size : Nat) ->

33+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

34+ so (src_offset + size <= src_init) ->

35+ RawMemory (MemoryChunk dst_size dst_init)

36+ (MemoryChunk dst_size (max dst_init (dst_offset + size))) ()

37+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (MemoryChunk n i)

3338

3439private

3540do_malloc : Nat -> IOExcept String Ptr

@@ -40,6 +45,12 @@ do_malloc size with (fromInteger (cast size) == size)

4045 else return ptr

4146 | False = ioe_fail "The target architecture does not support adressing enough memory"

4247

48+private

49+do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()

50+do_memset ptr offset c size

51+ = mkForeign (FFun "idris_memset" [FPtr, FInt, FAny Bits8, FInt] FUnit)

52+ ptr (cast offset) c (cast size)

53+

4354private

4455do_free : Ptr -> IO ()

4556do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr

@@ -68,72 +79,89 @@ do_poke ptr offset (b::bs)

6879instance Handler RawMemory (IOExcept String) where

6980 handle () (Allocate n) k

7081 = do ptr <- do_malloc n

71− k (CH ptr n) ()

72− handle (CH ptr n) (Free) k

82+ k (CH ptr) ()

83+ handle {res = MemoryChunk _ offset} (CH ptr) (Initialize c size _) k

84+ = ioe_lift (do_memset ptr offset c size) $> k (CH ptr) ()

85+ handle (CH ptr) (Free) k

7386 = ioe_lift (do_free ptr) $> k () ()

74− handle (CH ptr n) (Peek offset size _) k

87+ handle (CH ptr) (Peek offset size _) k

7588 = do res <- ioe_lift (do_peek ptr offset size)

76− k (CH ptr n) res

77− handle (CH ptr n) (Poke offset content _) k

89+ k (CH ptr) res

90+ handle (CH ptr) (Poke offset content _) k

7891 = do ioe_lift (do_poke ptr offset content)

79− k (CH ptr n) ()

80− handle (CH dest_ptr n) (Move (CH src_ptr m) dest_offset src_offset size _ _) k

92+ k (CH ptr) ()

93+ handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k

8194 = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)

82− k (CH dest_ptr n) ()

83− handle (CH ptr n) (GetRawPtr) k

84− = k (CH ptr n) (CH ptr n)

95+ k (CH dest_ptr) ()

96+ handle chunk (GetRawPtr) k

97+ = k chunk chunk

8598

8699RAW_MEMORY : Type -> EFFECT

87100RAW_MEMORY t = MkEff t RawMemory

88101

89−allocate : (n : Nat) -> EffM m [RAW_MEMORY ()] [RAW_MEMORY (MemoryChunk n)] ()

102+allocate : (n : Nat) -> EffM m [RAW_MEMORY ()] [RAW_MEMORY (MemoryChunk n 0)] ()

90103allocate size = Allocate size

91104

92−free : EffM m [RAW_MEMORY (MemoryChunk n)] [RAW_MEMORY ()] ()

105+initialize : {i : Nat} ->

106+ {n : Nat} ->

107+ Bits8 ->

108+ (size : Nat) ->

109+ so (i + size <= n) ->

110+ EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (i + size))] ()

111+initialize c size prf = Initialize c size prf

112+

113+free : EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY ()] ()

93114free = Free

94115

95−peek : {n : Nat} ->

116+peek : {i : Nat} ->

96117 (offset : Nat) ->

97118 (size : Nat) ->

98− so (offset + size <= n) ->

99− Eff m [RAW_MEMORY (MemoryChunk n)] (Vect Bits8 size)

119+ so (offset + size <= i) ->

120+ Eff m [RAW_MEMORY (MemoryChunk n i)] (Vect Bits8 size)

100121peek offset size prf = Peek offset size prf

101122

102123poke : {n : Nat} ->

124+ {i : Nat} ->

103125 (offset : Nat) ->

104126 Vect Bits8 size ->

105− so (offset + size <= n) ->

106− Eff m [RAW_MEMORY (MemoryChunk n)] ()

127+ so (offset <= i && offset + size <= n) ->

128+ EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (max i (offset + size)))] ()

107129poke offset content prf = Poke offset content prf

108130

109131private

110−getRawPtr : Eff m [RAW_MEMORY (MemoryChunk n)] (MemoryChunk n)

132+getRawPtr : Eff m [RAW_MEMORY (MemoryChunk n i)] (MemoryChunk n i)

111133getRawPtr = GetRawPtr

112134

113135private

114136move' : {dst_size : Nat} ->

115− {src_size : Nat} ->

116− (src_ptr : MemoryChunk src_size) ->

137+ {dst_init : Nat} ->

138+ {src_init : Nat} ->

139+ (src_ptr : MemoryChunk src_size src_init) ->

117140 (dst_offset : Nat) ->

118141 (src_offset : Nat) ->

119142 (size : Nat) ->

120− so (dst_offset + size <= dst_size) ->

121− so (src_offset + size <= src_size) ->

122− Eff m [RAW_MEMORY (MemoryChunk dst_size)] ()

143+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

144+ so (src_offset + size <= src_init) ->

145+ EffM m [RAW_MEMORY (MemoryChunk dst_size dst_init)]

146+ [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))] ()

123147move' src_ptr dst_offset src_offset size dst_bounds src_bounds

124148 = Move src_ptr dst_offset src_offset size dst_bounds src_bounds

125149

126150data MoveDescriptor = Dst | Src

127151

128152move : {dst_size : Nat} ->

153+ {dst_init : Nat} ->

129154 {src_size : Nat} ->

155+ {src_init : Nat} ->

130156 (dst_offset : Nat) ->

131157 (src_offset : Nat) ->

132158 (size : Nat) ->

133− so (dst_offset + size <= dst_size) ->

134− so (src_offset + size <= src_size) ->

135− Eff m [ Dst ::: RAW_MEMORY (MemoryChunk dst_size)

136− , Src ::: RAW_MEMORY (MemoryChunk src_size)] ()

159+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

160+ so (src_offset + size <= src_init) ->

161+ EffM m [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)

162+ , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]

163+ [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))

164+ , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)] ()

137165move dst_offset src_offset size dst_bounds src_bounds

138166 = do src_ptr <- Src :- getRawPtr

139167 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

java/src/main/java/org/idris/rts/ForeignPrimitives.java+10

@@ -195,6 +195,16 @@ public class ForeignPrimitives {

195195 return ByteBuffer.allocate(size);

196196 }

197197

198+ public static void idris_memset(Object buf, int offset, Object c, int size) {

199+ ByteBuffer buffer = (ByteBuffer)buf;

200+ buffer.rewind();

201+ buffer.position(offset);

202+ byte init[] = new byte[size];

203+ Arrays.fill(init, (Byte)c);

204+ buffer.put(init, offset, size);

205+ buffer.rewind();

206+ }

207+

198208 public static void free(Object buf) {

199209 buf = null;

200210 }

rts/idris_rts.c+32

@@ -186,6 +186,34 @@ VAL MKPTRc(VM* vm, void* ptr) {

186186 return cl;

187187}

188188

189+VAL MKB8(VM* vm, uint8_t bits8) {

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

191+ SETTY(cl, BITS8);

192+ cl -> info.bits8 = bits8;

193+ return cl;

194+}

195+

196+VAL MKB16(VM* vm, uint16_t bits16) {

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

198+ SETTY(cl, BITS16);

199+ cl -> info.bits16 = bits16;

200+ return cl;

201+}

202+

203+VAL MKB32(VM* vm, uint32_t bits32) {

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

205+ SETTY(cl, BITS32);

206+ cl -> info.bits32 = bits32;

207+ return cl;

208+}

209+

210+VAL MKB64(VM* vm, uint64_t bits64) {

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

212+ SETTY(cl, BITS64);

213+ cl -> info.bits64 = bits64;

214+ return cl;

215+}

216+

189217void PROJECT(VM* vm, VAL r, int loc, int arity) {

190218 int i;

191219 for(i = 0; i < arity; ++i) {

@@ -243,6 +271,10 @@ void dumpVal(VAL v) {

243271

244272}

245273

274+void idris_memset(void* ptr, i_int offset, VAL c, i_int size) {

275+ memset(((uint8_t*)ptr) + offset, c->info.bits8, size);

276+}

277+

246278int idris_peek(void* ptr, i_int offset) {

247279 uint8_t res = *(((uint8_t*)ptr) + offset);

248280 return (int)res;

rts/idris_rts.h+5

@@ -147,6 +147,10 @@ typedef intptr_t i_int;

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

148148VAL MKSTR(VM* vm, char* str);

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

150+VAL MKB8(VM* vm, uint8_t b);

151+VAL MKB16(VM* vm, uint16_t b);

152+VAL MKB32(VM* vm, uint32_t b);

153+VAL MKB64(VM* vm, uint64_t b);

150154

151155// following versions don't take a lock when allocating

152156VAL MKFLOATc(VM* vm, double val);

@@ -203,6 +207,7 @@ VAL idris_castFloatStr(VM* vm, VAL i);

203207VAL idris_castStrFloat(VM* vm, VAL i);

204208

205209// Raw memory manipulation

210+void idris_memset(void* ptr, i_int offset, VAL c, i_int size);

206211int idris_peek(void* ptr, i_int offset);

207212void idris_poke(void* ptr, i_int offset, VAL data);

208213void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size);

src/IRTS/CodegenC.hs+4

@@ -105,6 +105,10 @@ bcc i (ASSIGNCONST l c)

105105 mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"

106106 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"

107107 mkConst (Str s) = "MKSTR(vm, " ++ show s ++ ")"

108+ mkConst (B8 b) = "MKB8(vm, " ++ show b ++")"

109+ mkConst (B16 b) = "MKB16(vm, " ++ show b ++ ")"

110+ mkConst (B32 b) = "MKB32(vm, " ++ show b ++ ")"

111+ mkConst (B64 b) = "MKB64(vm, " ++ show b ++ ")"

108112 mkConst _ = "MKINT(42424242)"

109113bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

110114bcc i (MKCON l tag args)

src/IRTS/CodegenJava.hs+4−3

@@ -420,6 +420,7 @@ mkIdentifier (UN name) =

420420 cleanReserved "idris_assignStack" = "_idris_assignStack"

421421 cleanReserved "free" = "_free"

422422 cleanReserved "malloc" = "_malloc"

423+ cleanReserved "idris_memset" = "_idris_memset"

423424 cleanReserved "idris_peek" = "_idris_peek"

424425 cleanReserved "idris_poke" = "_idris_poke"

425426 cleanReserved "idris_memmove" = "_idris_memmove"

@@ -1238,10 +1239,10 @@ mkExp (SConst BIType) = return $ mkClass bigIntegerType

12381239mkExp (SConst FlType) = return $ mkClass doubleType

12391240mkExp (SConst ChType) = return $ mkClass charType

12401241mkExp (SConst StrType) = return $ mkClass stringType

1241−mkExp (SConst (B8 x)) = return $ mkPrimitive "Byte" (Int (toInteger x))

1242−mkExp (SConst (B16 x)) = return $ mkPrimitive "Short" (Int (toInteger x))

1242+mkExp (SConst (B8 x)) = return $ mkPrimitive "Byte" (String (show x))

1243+mkExp (SConst (B16 x)) = return $ mkPrimitive "Short" (String (show x))

12431244mkExp (SConst (B32 x)) = return $ mkPrimitive "Integer" (Int (toInteger x))

1244−mkExp (SConst (B64 x)) = return $ mkPrimitive "Long" (Int (toInteger x))

1245+mkExp (SConst (B64 x)) = return $ mkPrimitive "Long" (String (show x))

12451246mkExp (SConst (B8Type))= return $ mkClass byteType

12461247mkExp (SConst (B16Type)) = return $ mkClass shortType

12471248mkExp (SConst (B32Type)) = return $ mkClass integerType

test/test025/test025.idr+3−2

@@ -1,4 +1,4 @@

1−module Main

1+module Main

33import Effects

44import Effect.Memory

@@ -18,7 +18,8 @@ testMemory : MemoryIO () () (Vect Int 4)

1818testMemory = do Src :- allocate 5

1919 Src :- poke 0 inpVect oh

2020 Dst :- allocate 5

21− move 1 1 4 oh oh

21+ Dst :- initialize (prim__intToB8 1) 2 oh

22+ move 2 2 3 oh oh

2223 Src :- free

2324 end <- Dst :- peek 4 1 oh

2425 Dst :- poke 4 (sub1 end) oh