source: Deliverables/D2.2/8051/src/common/memory.ml @ 486

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

Deliverable D2.2

File size: 20.7 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
47(** This is the signature of the parameter module of the functor. *)
48
49module type DATA_SIZE =
50sig
51  val int_size  : int
52  val ptr_size  : int
53  val alignment : int option
54end
55
56
57(** This is the signature of the module that provides functions and types to
58    manipulate memories. *)
59
60module type S =
61sig
62
63  val mq_of_ptr : memory_q
64  val int_size  : int
65  val ptr_size  : int
66  val alignment : int option
67
68  module Value : Value.S
69
70  (* Memory. A memory contains values and function definitions. Since the memory
71     module will be used by the interpreters of the various languages of the
72     compilation chain, the type of memory is polymorphic with the type of
73     function definitions. *)
74
75  type 'fun_def memory
76
77  (* Memory manipulation *)
78
79  val empty : 'fun_def memory
80
81  (** [alloc mem size] allocates a block of [size] size (in bytes) in the memory
82      [mem]. It returns the new memory and a pointer to the beginning of the
83      allocated area. *)
84  val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.t
85
86  (* Memory free *)
87
88  val free : 'fun_def memory -> Value.t -> 'fun_def memory
89
90  (* Memory load and store *)
91
92  (** [load mem chunk addr] reads a value of type [chunk] at the address [addr]
93      in memory [mem]. *)
94  val load : 'fun_def memory -> memory_q -> Value.t -> Value.t
95  (** [load2 mem size addr] reads a value of size [size] at the address [addr]
96      in memory [mem]. *)
97  val load2 : 'fun_def memory -> int -> Value.t -> Value.t
98
99  (** [store mem chunk addr v] writes the value [v] interpreted as a value of
100      type [chunk] at address [addr] in memory [mem]. *)
101  val store  : 'fun_def memory -> memory_q -> Value.t -> Value.t ->
102               'fun_def memory
103  (** [store mem size addr v] writes the value [v] of size [size] at address
104      [addr] in memory [mem]. *)
105  val store2 : 'fun_def memory -> int -> Value.t -> Value.t ->
106               'fun_def memory
107
108  (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
109      memory [mem], and associates the global variable [x] with the address of
110      the block. *)
111  val add_var : 'fun_def memory -> AST.ident -> AST.data list -> 'fun_def memory
112
113  (** [add_fun_def mem f def] stores the function definition [def] in a new
114      block of memory [mem], and associates the function name [f] with the
115      address of the block. *)
116  val add_fun_def : 'fun_def memory -> AST.ident -> 'fun_def -> 'fun_def memory
117
118  (** [find_global mem x] returns the address associated with the global symbol
119      [x] in memory [mem]. [x] may be a global variable or the name of a
120      function. *)
121  val find_global : 'fun_def memory -> AST.ident -> Value.t
122
123  (** [find_fun_def mem addr] returns the function definition found at address
124      [addr] in memory [mem]. Raises an error if no function definition is
125      found. *)
126  val find_fun_def : 'fun_def memory -> Value.t -> 'fun_def
127
128  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
129      of size [sizes]. *)
130  val align : int (* starting offset *) -> int list (* sizes *) ->
131              (int list (* resulting offsets *) * int (* full size *))
132
133  val size_of_datas    : AST.data list -> int
134
135  (** [offsets_of_datas datas] returns the aligned offsets for the datas
136      [datas], starting at offset 0. *)
137  val offsets_of_datas : AST.data list -> (AST.data * int (* offset *)) list
138
139  val alloc_datas      : 'fun_def memory -> AST.data list ->
140                         ('fun_def memory * Value.t)
141
142  val print : 'fun_def memory -> unit
143
144end
145
146
147(** The functor to a memory module. *)
148
149module Make (D : DATA_SIZE) =
150struct
151
152  module Value = Value.Make (D)
153  module Block = Value.Block
154  module Offset = Value.Offset
155
156  let mq_of_ptr = MQ_pointer
157
158  let int_size = D.int_size
159  let ptr_size = D.ptr_size
160  let alignment = D.alignment
161
162
163  (* Contents of a variable. *)
164
165  type cell =
166    | Datum of int * Value.t (* the size of the content and its value *)
167    | Cont                   (* the continuation of a content defined in a
168                                previous block *)
169
170
171  module OffsetMap = Map.Make (Offset)
172  type offsetMap = cell OffsetMap.t
173  type offset = Offset.t
174
175  type contents =
176      { low   : offset ;
177        high  : offset ;
178        cells : offsetMap }
179
180  let update_cells contents cells = { contents with cells = cells }
181  let add_cells contents off v =
182    update_cells contents (OffsetMap.add off v contents.cells)
183
184  (* Alignment *)
185
186  let is_multiple n m = m mod n = 0
187
188  (** [align off size] returns the offset greater or equal to [off] that is
189      aligned for storing a value of size [size]. *)
190  let align off size = match D.alignment with
191    | None -> off
192    | Some alignment when (size <= alignment) && (is_multiple size alignment) ->
193      let size = Offset.of_int size in
194      let rem = Offset.modulo off size in
195      if Offset.eq rem Offset.zero then off
196      else Offset.add off (Offset.sub size rem)
197    | Some alignment ->
198      let size = Offset.of_int alignment in
199      let rem = Offset.modulo off size in
200      if Offset.eq rem Offset.zero then off
201      else Offset.add off (Offset.sub size rem)
202
203  let is_aligned off size = Offset.eq off (align off size)
204
205  (** [pad off] returns the offset that is obtained by adding some padding from
206      [off] and such that the result is aligned. *)
207  let pad off = match D.alignment with
208    | None -> off
209    | Some alignment -> align off alignment
210
211  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
212      of size [sizes]. *)
213  let align off sizes =
214    let rec aux (acc_offs, acc_size) off = function
215      | [] ->
216        let end_off = pad off in
217        let added_size = Offset.sub end_off off in
218        let added_size = Offset.to_int added_size in
219        (acc_offs, acc_size + added_size)
220      | size :: sizes ->
221        let aligned_off = align off size in
222        let next_off = Offset.add aligned_off (Offset.of_int size) in
223        let added_size = Offset.sub next_off off in
224        let added_size = Offset.to_int added_size in
225        let acc = (acc_offs @ [aligned_off], acc_size + added_size) in
226        aux acc next_off sizes
227    in
228    aux ([], 0) off sizes
229
230
231  (* Contents in memory. The type of function definitions varies from a language
232     to another; thus, it is left generic. *)
233
234  type 'fun_def content =
235    | Contents of contents
236    | Fun_def of 'fun_def
237
238
239  (* The mapping from blocks to contents. *)
240
241  module BlockMap = Map.Make (Block)
242  type 'fun_def blockMap = 'fun_def content BlockMap.t
243  type block = Block.t
244
245  (* The mapping from global identifiers to blocks (negative for function
246     definitions and positive for global variables). *)
247
248  module GlobalMap = Map.Make (String)
249  type globalMap = Value.t GlobalMap.t
250
251  (* The memory.
252     It is a mapping from blocks to contents, a mapping from global identifiers
253     (variables and functions) to pointers, a mapping from (negative) blocks to
254     function definition, the next free positive block and the next free
255     negative block. *)
256
257  type 'fun_def memory =
258      { blocks           : 'fun_def blockMap ;
259        addr_of_global   : globalMap ;
260        next_block       : block ;
261        next_fun_block   : block }
262
263  (* Pretty printing *)
264
265let print mem = 
266    let print_cells off = function
267      | Datum (size, v) when Value.eq v Value.undef -> 
268        ()
269      | Datum (size, v) -> 
270        Printf.printf "\n  %s: [%d,%s]%!"
271          (Offset.to_string off) size (Value.to_string v)
272      | Cont -> Printf.printf "[Cont]%!" in
273    let print_block b content =
274      Printf.printf "\nBlock %s: %!" (Block.to_string b) ;
275      match content with
276        | Contents contents ->
277            Printf.printf "(%s -> %s)%!"
278              (Offset.to_string contents.low) (Offset.to_string contents.high) ;
279            OffsetMap.iter print_cells contents.cells
280        | Fun_def _ -> Printf.printf "function definition%!" ;
281    in 
282    BlockMap.iter print_block mem.blocks ;
283    Printf.printf "\n%!"
284
285
286
287
288  (* Memory manipulation *)
289
290  let empty =
291    { blocks = BlockMap.empty ;
292      addr_of_global = GlobalMap.empty ;
293      next_block = Block.of_int 1 ;
294      next_fun_block = Block.of_int (-1) }
295
296  (* Memory allocation *)
297
298  (** [write_interval contents lo_off hi_off d] writes the cell [d] in the
299      contents [contents] from the offset [lo_off] (inclusive) to the offset
300      [hi_off] (exclusive). *)
301  let rec write_interval contents lo_off hi_off d =
302    if Offset.ge lo_off hi_off then contents
303    else
304      let contents = add_cells contents lo_off d in
305      write_interval contents (Offset.succ lo_off) hi_off d
306
307  (** [alloc2 mem lo hi] allocates in memory [mem] a new block whose readable
308      and writable offsets are the interval [lo] (inclusive) [hi]
309      (exclusive). *)
310  let alloc2 mem lo hi =
311    let b = mem.next_block in
312    let contents = { low = lo ; high = hi ; cells = OffsetMap.empty } in
313    let contents = write_interval contents lo hi (Datum (1, Value.undef)) in
314    let blocks = BlockMap.add b (Contents contents) mem.blocks in
315    let next_block = Block.succ mem.next_block in
316    let mem' = { mem with blocks = blocks ; next_block = next_block } in
317    (mem', Value.of_pointer (b, lo))
318
319  (** [alloc mem size] allocates a block of [size] size (in bytes) in the memory
320      [mem]. It returns the new memory and a pointer to the beginning of the
321      allocated area. *)
322  let alloc mem size =
323    alloc2 mem Offset.zero (Offset.of_int size)
324
325
326  let size_of_mq = function
327    | MQ_int8unsigned | MQ_int8signed -> 1
328    | MQ_int16unsigned | MQ_int16signed -> 2
329    | MQ_int32 | MQ_float32 -> 4
330    | MQ_float64 -> 8
331    | MQ_pointer -> D.ptr_size
332    | MQ_chunk -> D.ptr_size/2
333
334  let cast_of_mq = function
335    | MQ_int8unsigned -> Value.cast8unsigned
336    | MQ_int8signed -> Value.cast8signed
337    | MQ_int16unsigned -> Value.cast16unsigned
338    | MQ_int16signed -> Value.cast16signed
339    | MQ_int32 -> Value.cast32
340    | MQ_float32 | MQ_float64 -> error "float not supported."
341    | MQ_pointer | MQ_chunk -> (fun v -> v)
342
343  (* The 'safe'-prefixed functions below raise an error when the argument is not
344     of the expected form. *)
345
346  let safe_to_pointer msg v =
347    if Value.is_pointer v then Value.to_pointer v
348    else error msg
349
350  let safe_find msg find a map =
351    try find a map
352    with Not_found -> error msg
353
354  let safe_find_block msg b mem = safe_find msg BlockMap.find b mem.blocks
355
356  let safe_find_contents msg b mem = match safe_find_block msg b mem with
357    | Contents contents -> contents
358    | Fun_def _ -> error msg
359
360  let safe_find_offset msg off contents =
361    safe_find msg OffsetMap.find off contents.cells
362
363  let memory_find msg mem b off =
364    safe_find_offset msg off (safe_find_contents msg b mem)
365
366  (** [all_are_in_list msg mem b first_off last_off dl] returns [true] iff all
367      the datas found in the block [b] of memory [mem] and between offsets
368      [first_off] (inclusive) and [last_off] (exclusive) are in the list
369      [dl]. *)
370  let all_are_in_list msg mem b first_off last_off dl =
371    let d_eq d d' = match d, d' with
372      | Datum (size, v), Datum (size', v') -> (size = size') && (Value.eq v v')
373      | Cont, Cont -> true
374      | _ -> false in
375    let rec aux d = function
376      | [] -> false
377      | d' :: dl -> (d_eq d d') || (aux d dl) in
378    let dl_mem d = aux d dl in
379    match safe_find_block msg b mem with
380      | Contents contents
381          when (Offset.le contents.low first_off) &&
382            (Offset.le last_off contents.high) ->
383        let rec aux off =
384          if Offset.ge off last_off then true
385          else
386            if OffsetMap.mem off contents.cells then
387              let d = OffsetMap.find off contents.cells in
388              (dl_mem d) && (aux (Offset.succ off))
389            else false
390        in
391        aux first_off
392      | _ -> false
393
394  (** [all_are_undef msg mem b first_off last_off] returns [true] iff all the
395      datas found in the block [b] of memory [mem] and between offsets
396      [first_off] (inclusive) and [last_off] (exclusive) are the undef value. *)
397  let all_are_undef msg mem b first_off last_off =
398    all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef)]
399
400  (** [all_are_undef msg mem b first_off last_off] returns [true] iff all the
401      datas found in the block [b] of memory [mem] and between offsets
402      [first_off] (inclusive) and [last_off] (exclusive) are the undef value or
403      the Cont cell. *)
404  let all_are_undef_or_cont msg mem b first_off last_off =
405    all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef) ; Cont]
406
407  (** [write_value msg mem b off size v size'] store the value [v] at the offset
408      [off] of the block [b] in the memory [mem]. [size] is the size of the
409      value [v], and [size'] >= [size] is the number of bytes that are actually
410      written. When [size'] > [size], the undefined value is used to fill the
411      remaining memory cells. *)
412  let write_value msg mem b off size v size' =
413    if not (is_aligned off size) then
414      error "Alignment constraint violated when storing value."
415    else
416      let shift_off n = Offset.add off (Offset.of_int n) in
417      match safe_find_block msg b mem with
418        | Contents contents
419            when (Offset.le contents.low off) &&
420              (Offset.le (shift_off size) contents.high) ->
421          let contents = add_cells contents off (Datum (size, v)) in
422          let contents =
423            write_interval contents (Offset.succ off) (shift_off size) Cont in
424          let contents =
425            write_interval contents (shift_off size) (shift_off size')
426              (Datum (1, Value.undef)) in
427          let blocks = BlockMap.add b (Contents contents) mem.blocks in
428          { mem with blocks = blocks }
429        | _ -> error msg
430
431
432  (* Memory free *)
433
434  let free mem addr =
435    if Value.is_pointer addr then
436      let (b, _) = Value.to_pointer addr in
437      { mem with blocks = BlockMap.remove b mem.blocks }
438    else error "free: invalid memory address."
439
440
441  (* Memory load and store *)
442
443  (** [load2 mem size addr] reads a value of size [size] at the address [addr]
444      in memory [mem]. *)
445  let load2 mem size addr =
446    let msg = ("load: invalid memory access. ("^(Value.to_string addr)^")") in
447    let (b, off) = safe_to_pointer msg addr in
448    if not (is_aligned off size) then
449      error "Alignment constraint violated when loading value."
450    else
451      match memory_find msg mem b off with
452        | Datum (size', v) when size <= size' -> 
453          v
454              (*print_string ("Db: load m "^(string_of_memory_q chunk)^" "
455                            ^(Value.to_string addr)^" "^(Value.to_string r)^" ("
456                            ^(Value.to_string v)^")\n"); *)
457        | _ -> print mem;error msg
458
459  (** [load mem chunk addr] reads a value of type [chunk] at the address [addr]
460      in memory [mem]. *)
461  let load mem chunk addr =
462    let size = size_of_mq chunk in
463    cast_of_mq chunk (load2 mem size addr)
464
465
466  (** [write_undef_before msg mem b off] replaces with undefined values the
467      value whose last cell is at offset [off] of block [b] in memory
468      [mem]. *)
469  let write_undef_before msg mem b off =
470    let contents = safe_find_contents msg b mem in
471    let d = Datum (1, Value.undef) in
472    let rec aux off contents =
473      if OffsetMap.mem off contents.cells then
474        let contents' = add_cells contents off d in
475        match OffsetMap.find off contents.cells with
476          | Datum _ -> contents'
477          | Cont -> aux (Offset.pred off) contents'
478      else contents
479    in
480    let contents = aux off contents in
481    { mem with blocks = BlockMap.add b (Contents contents) mem.blocks }
482
483  (** [store2 mem size addr v] writes the value [v] of size [size] at address
484      [addr] in memory [mem]. *)
485  let store2 mem size addr v =
486    let msg = "store: invalid memory access." in
487    let (b, off) = safe_to_pointer msg addr in
488    let shift_off n = Offset.add off (Offset.of_int n) in
489    (*print_string ("Db: store m "^(string_of_memory_q chunk)^" "
490      ^(Value.to_string addr)^" "^(Value.to_string v)^" ("
491      ^(Value.to_string v0)^")\n"); *)
492    match memory_find msg mem b off with
493      | Datum (size', _) when size <= size' ->
494          write_value msg mem b off size v size'
495      | Datum (size', _)
496          when all_are_undef msg mem b (shift_off size') (shift_off size) ->
497          write_value msg mem b off size v size'
498      | Cont when all_are_undef_or_cont msg mem b off (shift_off size) ->
499          let mem = write_value msg mem b off size v size in 
500          write_undef_before msg mem b (Offset.pred off)
501      | _ -> error msg
502
503  (** [store mem chunk addr v] writes the value [v] interpreted as a value of
504      type [chunk] at address [addr] in memory [mem]. *)
505  let store mem chunk addr v =
506    store2 mem (size_of_mq chunk) addr (cast_of_mq chunk v)
507
508
509(* Data manipulation *)
510
511  let value_of_data = function
512    | AST.Data_reserve _ -> Value.undef
513    | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i -> Value.of_int i
514    | AST.Data_float32 f | AST.Data_float64 f -> Value.of_float f
515
516  let size_of_data = function
517    | AST.Data_reserve n -> n
518    | data -> size_of_mq (mq_of_data data)
519
520  let offsets_size_of_datas datas =
521    align Offset.zero (List.map size_of_data datas)
522
523  (** [alloc_datas mem datas] returns the memory and the address obtained by
524      allocating space and storing the datas [datas] in the memory [mem]. *)
525  let alloc_datas mem datas =
526    let (offs_of_datas, size) = offsets_size_of_datas datas in
527    let (mem, addr) = alloc mem size in
528    let shift_addr off = Value.add addr (Value.of_int_repr off) in
529    let f mem data off = match data with
530      | AST.Data_reserve _ -> mem
531      | _ -> store mem (mq_of_data data) (shift_addr off) (value_of_data data)
532    in
533    (List.fold_left2 f mem datas offs_of_datas, addr)
534
535  let size_of_datas datas = snd (offsets_size_of_datas datas)
536
537  (** [offsets_of_datas datas] returns the aligned offsets for the datas
538      [datas], starting at offset 0. *)
539  let offsets_of_datas datas =
540    let (offs_of_datas, _) = offsets_size_of_datas datas in
541    List.combine datas (List.map Offset.to_int offs_of_datas)
542
543  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
544      of size [sizes]. *)
545  let align off sizes =
546    let (offsets, size) = align (Offset.of_int off) sizes in
547    (List.map Offset.to_int offsets, size)
548
549
550  (* Global environment manipulation *)
551
552  (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
553      memory [mem], and associates the global variable [x] with the address of
554      the block. *)
555  let add_var mem v_id datas =
556    let (mem, addr) = alloc_datas mem datas in
557    let addr_of_global = GlobalMap.add v_id addr mem.addr_of_global in
558    { mem with addr_of_global = addr_of_global }
559
560  (** [add_fun_def mem f def] stores the function definition [def] in a new
561      block of memory [mem], and associates the function name [f] with the
562      address of the block. *)
563  let add_fun_def mem f_id f_def =
564    let b = mem.next_fun_block in
565    let next_fun_block = Block.pred mem.next_fun_block in
566    let addr = Value.of_pointer (b, Offset.zero) in
567    let addr_of_global = GlobalMap.add f_id addr mem.addr_of_global in
568    let blocks = BlockMap.add b (Fun_def f_def) mem.blocks in
569    { mem with blocks = blocks ;
570               addr_of_global = addr_of_global ;
571               next_fun_block = next_fun_block }
572
573  (** [find_global mem x] returns the address associated with the global symbol
574      [x] in memory [mem]. [x] may be a global variable or the name of a
575      function. *)
576  let find_global mem gid =
577    if GlobalMap.mem gid mem.addr_of_global then
578      GlobalMap.find gid mem.addr_of_global
579    else error ("Unknown global \"" ^ gid ^ "\"")
580
581  (** [find_fun_def mem addr] returns the function definition found at address
582      [addr] in memory [mem]. Raises an error if no function definition is
583      found. *)
584  let find_fun_def mem v =
585    let msg = "Invalid access to a function definition." in
586    let (b, _) = safe_to_pointer msg v in
587    match safe_find_block msg b mem with
588      | Contents _ -> error msg
589      | Fun_def def -> def
590
591
592 
593
594end
Note: See TracBrowser for help on using the repository browser.