source: Deliverables/D2.3/8051/src/common/memory.ml @ 453

Last change on this file since 453 was 453, checked in by ayache, 9 years ago

Import of the Paris's sources.

File size: 15.4 KB
Line 
1
2(** This file gives a memory model that can be used by the interpreter
3    of various languages throughout the compilation process and
4    following the memory model of the CompCert compiler. *)
5
6open IntValue
7
8
9let error_prefix = "Memory"
10let error s = Error.global_error error_prefix s
11
12
13(* Memory quantities are the size and the type of what can be loaded
14   and stored in memory *)
15
16type memory_q =
17  | MQ_int8signed | MQ_int8unsigned | MQ_int16signed | MQ_int16unsigned
18  | MQ_int32 | MQ_float32 | MQ_float64 | MQ_pointer | MQ_chunk
19
20let string_of_memory_q = function
21  | MQ_int8signed -> "int8s"
22  | MQ_int8unsigned -> "int8u"
23  | MQ_int16signed -> "int16s"
24  | MQ_int16unsigned -> "int16u"
25  | MQ_int32 -> "int32"
26  | MQ_float32 -> "float"
27  | MQ_float64 -> "float64"
28  | MQ_pointer -> "ptr"
29  | MQ_chunk -> "chunk"
30
31let mq_of_data = function
32  | AST.Data_reserve _ -> assert false (* Should not be called on this *)
33  | AST.Data_int8 _ -> MQ_int8signed
34  | AST.Data_int16 _ -> MQ_int16signed
35  | AST.Data_int32 _ -> MQ_int32
36  | AST.Data_float32 _ -> MQ_float32
37  | AST.Data_float64 _ -> MQ_float64
38
39let type_of_memory_q = function
40  | MQ_int8signed | MQ_int8unsigned | MQ_int16signed | MQ_int16unsigned
41  | MQ_int32 -> AST.Sig_int
42  | MQ_float32 | MQ_float64 -> AST.Sig_float
43  | MQ_pointer -> AST.Sig_ptr
44  | MQ_chunk -> error "Trying to get the type of a pointer chunk."
45
46
47module type DATA_SIZE =
48sig
49  val int_size  : int
50  val ptr_size  : int
51  val alignment : int option
52end
53
54
55module type S =
56sig
57
58  val mq_of_ptr : memory_q
59  val int_size  : int
60  val ptr_size  : int
61  val alignment : int option
62
63  module Value : Value.S
64
65  (* Memory *)
66
67  type 'fun_def memory
68
69  (* Memory manipulation *)
70
71  val empty : 'fun_def memory
72
73  (* Arguments are memory and size. *)
74  val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.t
75
76  (* Memory free *)
77
78  val free : 'fun_def memory -> Value.t -> 'fun_def memory
79
80  (* Memory load and store *)
81
82  (* Arguments are memory, memory quantity, pointer value.
83     A cast is performed on the value to load. *)
84  val load  : 'fun_def memory -> memory_q -> Value.t -> Value.t
85  (* Arguments are memory, size to load, pointer value. *)
86  val load2 : 'fun_def memory -> int -> Value.t -> Value.t
87
88  (* Arguments are memory, memory quantity, pointer Value.t, new value.
89     A cast is performed on the value to store. *)
90  val store : 'fun_def memory -> memory_q -> Value.t -> Value.t ->
91              'fun_def memory
92  (* Arguments are memory, size to store, pointer value, new value. *)
93  val store2 : 'fun_def memory -> int -> Value.t -> Value.t ->
94               'fun_def memory
95
96  val add_var : 'fun_def memory -> AST.ident -> AST.data list -> 'fun_def memory
97
98  val add_fun_def : 'fun_def memory -> AST.ident -> 'fun_def -> 'fun_def memory
99
100  val find_global : 'fun_def memory -> AST.ident -> Value.t
101
102  val find_fun_def : 'fun_def memory -> Value.t -> 'fun_def
103
104  val align : int (* starting offset *) -> int list (* sizes *) ->
105              (int list (* offsets *) * int (* full size *))
106
107  val size_of_datas    : AST.data list -> int
108  val offsets_of_datas : AST.data list -> (AST.data * int (* offset *)) list
109  val alloc_datas      : 'fun_def memory -> AST.data list ->
110                         ('fun_def memory * Value.t)
111
112  val print : 'fun_def memory -> unit
113
114end
115
116
117module Make (D : DATA_SIZE) =
118struct
119
120  module Value = Value.Make (D)
121  module Block = Value.Block
122  module Offset = Value.Offset
123
124  let mq_of_ptr = MQ_pointer
125
126  let int_size = D.int_size
127  let ptr_size = D.ptr_size
128  let alignment = D.alignment
129
130
131  (* Contents of a variable. *)
132
133  type cell =
134    | Datum of int * Value.t (* the size of the content and its value *)
135    | Cont                   (* the continuation of a content defined in a
136                                previous block *)
137
138
139  module OffsetMap = Map.Make (Offset)
140  type offsetMap = cell OffsetMap.t
141  type offset = Offset.t
142
143  type contents =
144      { low   : offset ;
145        high  : offset ;
146        cells : offsetMap }
147
148  let update_cells contents cells = { contents with cells = cells }
149  let add_cells contents off v =
150    update_cells contents (OffsetMap.add off v contents.cells)
151
152  (* Alignment *)
153
154  let is_multiple n m = m mod n = 0
155
156  let align off size = match D.alignment with
157    | None -> off
158    | Some alignment when (size <= alignment) && (is_multiple size alignment) ->
159        let size = Offset.of_int size in
160        let rem = Offset.modulo off size in
161        if Offset.eq rem Offset.zero then off
162        else Offset.add off (Offset.sub size rem)
163    | Some alignment ->
164        let size = Offset.of_int alignment in
165        let rem = Offset.modulo off size in
166        if Offset.eq rem Offset.zero then off
167        else Offset.add off (Offset.sub size rem)
168
169  let is_aligned off size = Offset.eq off (align off size)
170
171  let pad off = match D.alignment with
172    | None -> off
173    | Some alignment -> align off alignment
174
175  let align off sizes =
176    let rec aux (acc_offs, acc_size) off = function
177      | [] ->
178          let end_off = pad off in
179          let added_size = Offset.sub end_off off in
180          let added_size = Offset.to_int added_size in
181          (acc_offs, acc_size + added_size)
182      | size :: sizes ->
183          let aligned_off = align off size in
184          let next_off = Offset.add aligned_off (Offset.of_int size) in
185          let added_size = Offset.sub next_off off in
186          let added_size = Offset.to_int added_size in
187          let acc = (acc_offs @ [aligned_off], acc_size + added_size) in
188          aux acc next_off sizes
189    in
190    aux ([], 0) off sizes
191
192
193  (* Contents in memory. The type of function definitions varies from a language
194     to another; thus, it is left generic. *)
195
196  type 'fun_def content =
197    | Contents of contents
198    | Fun_def of 'fun_def
199
200
201  (* The mapping from blocks to contents. *)
202
203  module BlockMap = Map.Make (Block)
204  type 'fun_def blockMap = 'fun_def content BlockMap.t
205  type block = Block.t
206
207  (* The mapping from global identifiers to blocks (negative for function
208     definitions and positive for global variables). *)
209
210  module GlobalMap = Map.Make (String)
211  type globalMap = Value.t GlobalMap.t
212
213  (* The memory.
214     It is a mapping from blocks to contents, a mapping from global identifiers
215     (variables and functions) to pointers, a mapping from (negative) blocks to
216     function definition, the next free positive block and the next free
217     negative block. *)
218
219  type 'fun_def memory =
220      { blocks           : 'fun_def blockMap ;
221        addr_of_global   : globalMap ;
222        next_block       : block ;
223        next_fun_block   : block }
224
225
226  (* Memory manipulation *)
227
228  let empty =
229    { blocks = BlockMap.empty ;
230      addr_of_global = GlobalMap.empty ;
231      next_block = Block.of_int 1 ;
232      next_fun_block = Block.of_int (-1) }
233
234  (* Memory allocation *)
235
236  let rec write_interval contents lo_off hi_off d =
237    if Offset.ge lo_off hi_off then contents
238    else
239      let contents = add_cells contents lo_off d in
240      write_interval contents (Offset.succ lo_off) hi_off d
241
242  let alloc2 mem lo hi =
243    let b = mem.next_block in
244    let contents = { low = lo ; high = hi ; cells = OffsetMap.empty } in
245    let contents = write_interval contents lo hi (Datum (1, Value.undef)) in
246    let blocks = BlockMap.add b (Contents contents) mem.blocks in
247    let next_block = Block.succ mem.next_block in
248    let mem' = { mem with blocks = blocks ; next_block = next_block } in
249    (mem', Value.of_pointer (b, lo))
250
251  let alloc mem size =
252    alloc2 mem Offset.zero (Offset.of_int size)
253
254
255  let size_of_mq = function
256    | MQ_int8unsigned | MQ_int8signed -> 1
257    | MQ_int16unsigned | MQ_int16signed -> 2
258    | MQ_int32 | MQ_float32 -> 4
259    | MQ_float64 -> 8
260    | MQ_pointer -> D.ptr_size
261    | MQ_chunk -> D.ptr_size/2
262
263  let cast_of_mq = function
264    | MQ_int8unsigned -> Value.cast8unsigned
265    | MQ_int8signed -> Value.cast8signed
266    | MQ_int16unsigned -> Value.cast16unsigned
267    | MQ_int16signed -> Value.cast16signed
268    | MQ_int32 -> Value.cast32
269    | MQ_float32 | MQ_float64 -> error "float not supported."
270    | MQ_pointer | MQ_chunk -> (fun v -> v)
271
272  let safe_to_pointer msg v =
273    if Value.is_pointer v then Value.to_pointer v
274    else error msg
275
276  let safe_find msg find a map =
277    try find a map
278    with Not_found -> error msg
279
280  let safe_find_block msg b mem = safe_find msg BlockMap.find b mem.blocks
281
282  let safe_find_contents msg b mem = match safe_find_block msg b mem with
283    | Contents contents -> contents
284    | Fun_def _ -> error msg
285
286  let safe_find_offset msg off contents =
287    safe_find msg OffsetMap.find off contents.cells
288
289  let memory_find msg mem b off =
290    safe_find_offset msg off (safe_find_contents msg b mem)
291
292  let all_are_in_list msg mem b first_off last_off dl =
293    let d_eq d d' = match d, d' with
294      | Datum (size, v), Datum (size', v') -> (size = size') && (Value.eq v v')
295      | Cont, Cont -> true
296      | _ -> false in
297    let rec aux d = function
298      | [] -> false
299      | d' :: dl -> (d_eq d d') || (aux d dl) in
300    let dl_mem d = aux d dl in
301    match safe_find_block msg b mem with
302      | Contents contents
303          when (Offset.le contents.low first_off) &&
304               (Offset.le last_off contents.high) ->
305          let rec aux off =
306            if Offset.ge off last_off then true
307            else
308              if OffsetMap.mem off contents.cells then
309                let d = OffsetMap.find off contents.cells in
310                (dl_mem d) && (aux (Offset.succ off))
311              else false
312          in
313          aux first_off
314      | _ -> false
315
316  let all_are_undef msg mem b first_off last_off =
317    all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef)]
318
319  let all_are_undef_or_cont msg mem b first_off last_off =
320    all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef) ; Cont]
321
322  let write_value msg mem b off size v size' =
323    if not (is_aligned off size) then
324      error "Alignment constraint violated when storing value."
325    else
326      let shift_off n = Offset.add off (Offset.of_int n) in
327      match safe_find_block msg b mem with
328        | Contents contents
329            when (Offset.le contents.low off) &&
330                 (Offset.le (shift_off size) contents.high) ->
331            let contents = add_cells contents off (Datum (size, v)) in
332            let contents =
333              write_interval contents (Offset.succ off) (shift_off size) Cont in
334            let contents =
335              write_interval contents (shift_off size) (shift_off size')
336                (Datum (1, Value.undef)) in
337            let blocks = BlockMap.add b (Contents contents) mem.blocks in
338            { mem with blocks = blocks }
339        | _ -> error msg
340
341
342  (* Memory free *)
343
344  let free mem addr =
345    if Value.is_pointer addr then
346      let (b, _) = Value.to_pointer addr in
347      { mem with blocks = BlockMap.remove b mem.blocks }
348    else error "free: invalid memory address."
349
350
351  (* Memory load and store *)
352
353  let load2 mem size addr =
354    let msg = ("load: invalid memory access. ("^(Value.to_string addr)^")") in
355    let (b, off) = safe_to_pointer msg addr in
356    if not (is_aligned off size) then
357      error "Alignment constraint violated when loading value."
358    else
359      match memory_find msg mem b off with
360        | Datum (size', v) when size <= size' -> 
361          v
362              (*print_string ("Db: load m "^(string_of_memory_q chunk)^" "
363                            ^(Value.to_string addr)^" "^(Value.to_string r)^" ("
364                            ^(Value.to_string v)^")\n"); *)
365        | _ -> error msg
366
367  let load mem chunk addr =
368    let size = size_of_mq chunk in
369    cast_of_mq chunk (load2 mem size addr)
370
371
372  let write_undef_before msg mem b off =
373    let contents = safe_find_contents msg b mem in
374    let d = Datum (1, Value.undef) in
375    let rec aux off contents =
376      if OffsetMap.mem off contents.cells then
377        let contents = add_cells contents off d in
378        match OffsetMap.find off contents.cells with
379          | Datum _ -> contents
380          | Cont -> aux (Offset.pred off) contents
381      else contents
382    in
383    let contents = aux off contents in
384    { mem with blocks = BlockMap.add b (Contents contents) mem.blocks }
385
386  let store2 mem size addr v =
387    let msg = "store: invalid memory access." in
388    let (b, off) = safe_to_pointer msg addr in
389    let shift_off n = Offset.add off (Offset.of_int n) in
390      (*print_string ("Db: store m "^(string_of_memory_q chunk)^" "
391                    ^(Value.to_string addr)^" "^(Value.to_string v)^" ("
392                    ^(Value.to_string v0)^")\n"); *)
393    match memory_find msg mem b off with
394      | Datum (size', _) when size <= size' ->
395          write_value msg mem b off size v size'
396      | Datum (size', _)
397          when all_are_undef msg mem b (shift_off size') (shift_off size) ->
398          write_value msg mem b off size v size'
399      | Cont when all_are_undef_or_cont msg mem b off (shift_off size) ->
400          let mem = write_value msg mem b off size v size in 
401          write_undef_before msg mem b (Offset.pred off)
402      | _ -> error msg
403
404  let store mem chunk addr v =
405    store2 mem (size_of_mq chunk) addr (cast_of_mq chunk v)
406
407
408(* Data manipulation *)
409
410  let value_of_data = function
411    | AST.Data_reserve _ -> Value.undef
412    | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i -> Value.of_int i
413    | AST.Data_float32 f | AST.Data_float64 f -> Value.of_float f
414
415  let size_of_data = function
416    | AST.Data_reserve n -> n
417    | data -> size_of_mq (mq_of_data data)
418
419  let offsets_size_of_datas datas =
420    align Offset.zero (List.map size_of_data datas)
421
422  let alloc_datas mem datas =
423    let (offs_of_datas, size) = offsets_size_of_datas datas in
424    let (mem, addr) = alloc mem size in
425    let shift_addr off = Value.add addr (Value.of_int_repr off) in
426    let f mem data off = match data with
427      | AST.Data_reserve _ -> mem
428      | _ -> store mem (mq_of_data data) (shift_addr off) (value_of_data data)
429    in
430    (List.fold_left2 f mem datas offs_of_datas, addr)
431
432  let size_of_datas datas = snd (offsets_size_of_datas datas)
433
434  let offsets_of_datas datas =
435    let (offs_of_datas, _) = offsets_size_of_datas datas in
436    List.combine datas (List.map Offset.to_int offs_of_datas)
437
438  let align off sizes =
439    let (offsets, size) = align (Offset.of_int off) sizes in
440    (List.map Offset.to_int offsets, size)
441
442
443  (* Global environment manipulation *)
444
445  let add_var mem v_id datas =
446    let (mem, addr) = alloc_datas mem datas in
447    let addr_of_global = GlobalMap.add v_id addr mem.addr_of_global in
448    { mem with addr_of_global = addr_of_global }
449
450  let add_fun_def mem f_id f_def =
451    let b = mem.next_fun_block in
452    let next_fun_block = Block.pred mem.next_fun_block in
453    let addr = Value.of_pointer (b, Offset.zero) in
454    let addr_of_global = GlobalMap.add f_id addr mem.addr_of_global in
455    let blocks = BlockMap.add b (Fun_def f_def) mem.blocks in
456    { mem with blocks = blocks ;
457               addr_of_global = addr_of_global ;
458               next_fun_block = next_fun_block }
459
460  let find_global mem gid =
461    if GlobalMap.mem gid mem.addr_of_global then
462      GlobalMap.find gid mem.addr_of_global
463    else error ("Unknown global \"" ^ gid ^ "\"")
464
465  let find_fun_def mem v =
466    let msg = "Invalid access to a function definition." in
467    let (b, _) = safe_to_pointer msg v in
468    match safe_find_block msg b mem with
469      | Contents _ -> error msg
470      | Fun_def def -> def
471
472
473  let print mem = 
474    let print_cells off = function
475      | Datum (size, v) when Value.eq v Value.undef -> 
476        ()
477      | Datum (size, v) -> 
478        Printf.printf "\n  %s: [%d,%s]%!"
479          (Offset.to_string off) size (Value.to_string v)
480      | Cont -> Printf.printf "[Cont]%!" in
481    let print_block b content =
482      Printf.printf "\nBlock %s: %!" (Block.to_string b) ;
483      match content with
484        | Contents contents ->
485            Printf.printf "(%s -> %s)%!"
486              (Offset.to_string contents.low) (Offset.to_string contents.high) ;
487            OffsetMap.iter print_cells contents.cells
488        | Fun_def _ -> Printf.printf "function definition%!" ;
489    in 
490    BlockMap.iter print_block mem.blocks ;
491    Printf.printf "\n%!"
492
493end
Note: See TracBrowser for help on using the repository browser.