git.iko.soy/Idris-dev
on master help sign in
Proper initialization semantics for raw memory
e294e0eJan Bessai
effects/Effect/Memory.idr+76−48
compare with master
unifiedsplit
@@ -6,30 +6,35 @@ import Control.IOExcept
6%access public
6%access public
7
7
8abstract
8abstract
9−data MemoryChunk : Nat -> Type where
9+data MemoryChunk : Nat -> Nat -> Type where
10− CH : Ptr -> (size : Nat) -> MemoryChunk size
10+ CH : Ptr -> MemoryChunk size initialized
11
11
12abstract
12abstract
13data RawMemory : Effect where
13data RawMemory : Effect where
14− Allocate : (n : Nat) ->
14+ Allocate : (n : Nat) ->
15− RawMemory () (MemoryChunk n) ()
15+ RawMemory () (MemoryChunk n 0) ()
16− Free : RawMemory (MemoryChunk n) () ()
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)) ()
17− Peek : (offset : Nat) ->
21+ Peek : (offset : Nat) ->
18− (size : Nat) ->
22+ (size : Nat) ->
19− so (offset + size <= n) ->
23+ so (offset + size <= i) ->
20− RawMemory (MemoryChunk n) (MemoryChunk n) (Vect Bits8 size)
24+ RawMemory (MemoryChunk n i) (MemoryChunk n i) (Vect Bits8 size)
21− Poke : (offset : Nat) ->
25+ Poke : (offset : Nat) ->
22− (Vect Bits8 size) ->
26+ (Vect Bits8 size) ->
23− so (offset + size <= n) ->
27+ so (offset <= i && offset + size <= n) ->
24− RawMemory (MemoryChunk n) (MemoryChunk n) ()
28+ RawMemory (MemoryChunk n i) (MemoryChunk n (max i (offset + size))) ()
25− Move : (src : MemoryChunk m) ->
29+ Move : (src : MemoryChunk src_size src_init) ->
26− (dest_offset : Nat) ->
30+ (dst_offset : Nat) ->
27− (src_offset : Nat) ->
31+ (src_offset : Nat) ->
28− (size : Nat) ->
32+ (size : Nat) ->
29− so (dest_offset + size <= n) ->
33+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
30− so (src_offset + size <= m) ->
34+ so (src_offset + size <= src_init) ->
31− RawMemory (MemoryChunk n) (MemoryChunk n) ()
35+ RawMemory (MemoryChunk dst_size dst_init)
36+ (MemoryChunk dst_size (max dst_init (dst_offset + size))) ()
32− GetRawPtr : RawMemory (MemoryChunk n) (MemoryChunk n) (MemoryChunk n)
37+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (MemoryChunk n i)
33
38
34private
39private
35do_malloc : Nat -> IOExcept String Ptr
40do_malloc : Nat -> IOExcept String Ptr
@@ -40,6 +45,12 @@ do_malloc size with (fromInteger (cast size) == size)
40 else return ptr
45 else return ptr
41 | False = ioe_fail "The target architecture does not support adressing enough memory"
46 | False = ioe_fail "The target architecture does not support adressing enough memory"
42
47
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+
43private
54private
44do_free : Ptr -> IO ()
55do_free : Ptr -> IO ()
45do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr
56do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr
@@ -68,72 +79,89 @@ do_poke ptr offset (b::bs)
68instance Handler RawMemory (IOExcept String) where
79instance Handler RawMemory (IOExcept String) where
69 handle () (Allocate n) k
80 handle () (Allocate n) k
70 = do ptr <- do_malloc n
81 = do ptr <- do_malloc n
71− k (CH ptr n) ()
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) ()
72− handle (CH ptr n) (Free) k
85+ handle (CH ptr) (Free) k
73 = ioe_lift (do_free ptr) $> k () ()
86 = ioe_lift (do_free ptr) $> k () ()
74− handle (CH ptr n) (Peek offset size _) k
87+ handle (CH ptr) (Peek offset size _) k
75 = do res <- ioe_lift (do_peek ptr offset size)
88 = do res <- ioe_lift (do_peek ptr offset size)
76− k (CH ptr n) res
89+ k (CH ptr) res
77− handle (CH ptr n) (Poke offset content _) k
90+ handle (CH ptr) (Poke offset content _) k
78 = do ioe_lift (do_poke ptr offset content)
91 = do ioe_lift (do_poke ptr offset content)
79− k (CH ptr n) ()
92+ k (CH ptr) ()
80− handle (CH dest_ptr n) (Move (CH src_ptr m) dest_offset src_offset size _ _) k
93+ handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k
81 = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)
94 = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)
82− k (CH dest_ptr n) ()
95+ k (CH dest_ptr) ()
83− handle (CH ptr n) (GetRawPtr) k
96+ handle chunk (GetRawPtr) k
84− = k (CH ptr n) (CH ptr n)
97+ = k chunk chunk
85
98
86RAW_MEMORY : Type -> EFFECT
99RAW_MEMORY : Type -> EFFECT
87RAW_MEMORY t = MkEff t RawMemory
100RAW_MEMORY t = MkEff t RawMemory
88
101
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)] ()
90allocate size = Allocate size
103allocate size = Allocate size
91
104
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+
92−free : EffM m [RAW_MEMORY (MemoryChunk n)] [RAW_MEMORY ()] ()
113+free : EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY ()] ()
93free = Free
114free = Free
94
115
95−peek : {n : Nat} ->
116+peek : {i : Nat} ->
96 (offset : Nat) ->
117 (offset : Nat) ->
97 (size : Nat) ->
118 (size : Nat) ->
98− so (offset + size <= n) ->
119+ so (offset + size <= i) ->
99− Eff m [RAW_MEMORY (MemoryChunk n)] (Vect Bits8 size)
120+ Eff m [RAW_MEMORY (MemoryChunk n i)] (Vect Bits8 size)
100peek offset size prf = Peek offset size prf
121peek offset size prf = Peek offset size prf
101
122
102poke : {n : Nat} ->
123poke : {n : Nat} ->
124+ {i : Nat} ->
103 (offset : Nat) ->
125 (offset : Nat) ->
104 Vect Bits8 size ->
126 Vect Bits8 size ->
105− so (offset + size <= n) ->
127+ so (offset <= i && offset + size <= n) ->
106− Eff m [RAW_MEMORY (MemoryChunk n)] ()
128+ EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (max i (offset + size)))] ()
107poke offset content prf = Poke offset content prf
129poke offset content prf = Poke offset content prf
108
130
109private
131private
110−getRawPtr : Eff m [RAW_MEMORY (MemoryChunk n)] (MemoryChunk n)
132+getRawPtr : Eff m [RAW_MEMORY (MemoryChunk n i)] (MemoryChunk n i)
111getRawPtr = GetRawPtr
133getRawPtr = GetRawPtr
112
134
113private
135private
114move' : {dst_size : Nat} ->
136move' : {dst_size : Nat} ->
115− {src_size : Nat} ->
137+ {dst_init : Nat} ->
138+ {src_init : Nat} ->
116− (src_ptr : MemoryChunk src_size) ->
139+ (src_ptr : MemoryChunk src_size src_init) ->
117 (dst_offset : Nat) ->
140 (dst_offset : Nat) ->
118 (src_offset : Nat) ->
141 (src_offset : Nat) ->
119 (size : Nat) ->
142 (size : Nat) ->
120− so (dst_offset + size <= dst_size) ->
143+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
121− so (src_offset + size <= src_size) ->
144+ so (src_offset + size <= src_init) ->
122− Eff m [RAW_MEMORY (MemoryChunk dst_size)] ()
145+ EffM m [RAW_MEMORY (MemoryChunk dst_size dst_init)]
146+ [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))] ()
123move' src_ptr dst_offset src_offset size dst_bounds src_bounds
147move' src_ptr dst_offset src_offset size dst_bounds src_bounds
124 = Move src_ptr dst_offset src_offset size dst_bounds src_bounds
148 = Move src_ptr dst_offset src_offset size dst_bounds src_bounds
125
149
126data MoveDescriptor = Dst | Src
150data MoveDescriptor = Dst | Src
127
151
128move : {dst_size : Nat} ->
152move : {dst_size : Nat} ->
153+ {dst_init : Nat} ->
129 {src_size : Nat} ->
154 {src_size : Nat} ->
155+ {src_init : Nat} ->
130 (dst_offset : Nat) ->
156 (dst_offset : Nat) ->
131 (src_offset : Nat) ->
157 (src_offset : Nat) ->
132 (size : Nat) ->
158 (size : Nat) ->
133− so (dst_offset + size <= dst_size) ->
159+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
134− so (src_offset + size <= src_size) ->
160+ so (src_offset + size <= src_init) ->
135− Eff m [ Dst ::: RAW_MEMORY (MemoryChunk dst_size)
161+ EffM m [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)
136− , Src ::: RAW_MEMORY (MemoryChunk src_size)] ()
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)] ()
137move dst_offset src_offset size dst_bounds src_bounds
165move dst_offset src_offset size dst_bounds src_bounds
138 = do src_ptr <- Src :- getRawPtr
166 = do src_ptr <- Src :- getRawPtr
139 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
167 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 {
195 return ByteBuffer.allocate(size);
195 return ByteBuffer.allocate(size);
196 }
196 }
197
197
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+
198 public static void free(Object buf) {
208 public static void free(Object buf) {
199 buf = null;
209 buf = null;
200 }
210 }
rts/idris_rts.c+32
@@ -186,6 +186,34 @@ VAL MKPTRc(VM* vm, void* ptr) {
186 return cl;
186 return cl;
187}
187}
188
188
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+
189void PROJECT(VM* vm, VAL r, int loc, int arity) {
217void PROJECT(VM* vm, VAL r, int loc, int arity) {
190 int i;
218 int i;
191 for(i = 0; i < arity; ++i) {
219 for(i = 0; i < arity; ++i) {
@@ -243,6 +271,10 @@ void dumpVal(VAL v) {
243
271
244}
272}
245
273
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+
246int idris_peek(void* ptr, i_int offset) {
278int idris_peek(void* ptr, i_int offset) {
247 uint8_t res = *(((uint8_t*)ptr) + offset);
279 uint8_t res = *(((uint8_t*)ptr) + offset);
248 return (int)res;
280 return (int)res;
rts/idris_rts.h+5
@@ -147,6 +147,10 @@ typedef intptr_t i_int;
147VAL MKFLOAT(VM* vm, double val);
147VAL MKFLOAT(VM* vm, double val);
148VAL MKSTR(VM* vm, char* str);
148VAL MKSTR(VM* vm, char* str);
149VAL MKPTR(VM* vm, void* ptr);
149VAL 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);
150
154
151// following versions don't take a lock when allocating
155// following versions don't take a lock when allocating
152VAL MKFLOATc(VM* vm, double val);
156VAL MKFLOATc(VM* vm, double val);
@@ -203,6 +207,7 @@ VAL idris_castFloatStr(VM* vm, VAL i);
203VAL idris_castStrFloat(VM* vm, VAL i);
207VAL idris_castStrFloat(VM* vm, VAL i);
204
208
205// Raw memory manipulation
209// Raw memory manipulation
210+void idris_memset(void* ptr, i_int offset, VAL c, i_int size);
206int idris_peek(void* ptr, i_int offset);
211int idris_peek(void* ptr, i_int offset);
207void idris_poke(void* ptr, i_int offset, VAL data);
212void idris_poke(void* ptr, i_int offset, VAL data);
208void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size);
213void 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)
105 mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"
105 mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"
106 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"
106 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"
107 mkConst (Str s) = "MKSTR(vm, " ++ show s ++ ")"
107 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 ++ ")"
108 mkConst _ = "MKINT(42424242)"
112 mkConst _ = "MKINT(42424242)"
109bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
113bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
110bcc i (MKCON l tag args)
114bcc i (MKCON l tag args)
src/IRTS/CodegenJava.hs+4−3
@@ -420,6 +420,7 @@ mkIdentifier (UN name) =
420 cleanReserved "idris_assignStack" = "_idris_assignStack"
420 cleanReserved "idris_assignStack" = "_idris_assignStack"
421 cleanReserved "free" = "_free"
421 cleanReserved "free" = "_free"
422 cleanReserved "malloc" = "_malloc"
422 cleanReserved "malloc" = "_malloc"
423+ cleanReserved "idris_memset" = "_idris_memset"
423 cleanReserved "idris_peek" = "_idris_peek"
424 cleanReserved "idris_peek" = "_idris_peek"
424 cleanReserved "idris_poke" = "_idris_poke"
425 cleanReserved "idris_poke" = "_idris_poke"
425 cleanReserved "idris_memmove" = "_idris_memmove"
426 cleanReserved "idris_memmove" = "_idris_memmove"
@@ -1238,10 +1239,10 @@ mkExp (SConst BIType) = return $ mkClass bigIntegerType
1238mkExp (SConst FlType) = return $ mkClass doubleType
1239mkExp (SConst FlType) = return $ mkClass doubleType
1239mkExp (SConst ChType) = return $ mkClass charType
1240mkExp (SConst ChType) = return $ mkClass charType
1240mkExp (SConst StrType) = return $ mkClass stringType
1241mkExp (SConst StrType) = return $ mkClass stringType
1241−mkExp (SConst (B8 x)) = return $ mkPrimitive "Byte" (Int (toInteger x))
1242+mkExp (SConst (B8 x)) = return $ mkPrimitive "Byte" (String (show x))
1242−mkExp (SConst (B16 x)) = return $ mkPrimitive "Short" (Int (toInteger x))
1243+mkExp (SConst (B16 x)) = return $ mkPrimitive "Short" (String (show x))
1243mkExp (SConst (B32 x)) = return $ mkPrimitive "Integer" (Int (toInteger x))
1244mkExp (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))
1245mkExp (SConst (B8Type))= return $ mkClass byteType
1246mkExp (SConst (B8Type))= return $ mkClass byteType
1246mkExp (SConst (B16Type)) = return $ mkClass shortType
1247mkExp (SConst (B16Type)) = return $ mkClass shortType
1247mkExp (SConst (B32Type)) = return $ mkClass integerType
1248mkExp (SConst (B32Type)) = return $ mkClass integerType
test/test025/test025.idr+3−2
@@ -1,4 +1,4 @@
1−module Main
1+module Main
2
2
3import Effects
3import Effects
4import Effect.Memory
4import Effect.Memory
@@ -18,7 +18,8 @@ testMemory : MemoryIO () () (Vect Int 4)
18testMemory = do Src :- allocate 5
18testMemory = do Src :- allocate 5
19 Src :- poke 0 inpVect oh
19 Src :- poke 0 inpVect oh
20 Dst :- allocate 5
20 Dst :- allocate 5
21+ Dst :- initialize (prim__intToB8 1) 2 oh
21− move 1 1 4 oh oh
22+ move 2 2 3 oh oh
22 Src :- free
23 Src :- free
23 end <- Dst :- peek 4 1 oh
24 end <- Dst :- peek 4 1 oh
24 Dst :- poke 4 (sub1 end) oh
25 Dst :- poke 4 (sub1 end) oh