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

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

Update of D2.2 from Paris.

File size: 20.8 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.modulou 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.modulou 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
265  let 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  (* Memory manipulation *)
287
288  let empty =
289    { blocks = BlockMap.empty ;
290      addr_of_global = GlobalMap.empty ;
291      next_block = Block.of_int 1 ;
292      next_fun_block = Block.of_int (-1) }
293
294  (* Memory allocation *)
295
296  (** [write_interval contents lo_off hi_off d] writes the cell [d] in the
297      contents [contents] from the offset [lo_off] (inclusive) to the offset
298      [hi_off] (exclusive). *)
299  let rec write_interval contents lo_off hi_off d =
300    if Offset.ge lo_off hi_off then contents
301    else
302      let contents = add_cells contents lo_off d in
303      write_interval contents (Offset.succ lo_off) hi_off d
304
305  (** [alloc2 mem lo hi] allocates in memory [mem] a new block whose readable
306      and writable offsets are the interval [lo] (inclusive) [hi]
307      (exclusive). *)
308  let alloc2 mem lo hi =
309    let b = mem.next_block in
310    let contents = { low = lo ; high = hi ; cells = OffsetMap.empty } in
311    let contents = write_interval contents lo hi (Datum (1, Value.undef)) in
312    let blocks = BlockMap.add b (Contents contents) mem.blocks in
313    let next_block = Block.succ mem.next_block in
314    let mem' = { mem with blocks = blocks ; next_block = next_block } in
315    (mem', Value.of_pointer (b, lo))
316
317  (** [alloc mem size] allocates a block of [size] size (in bytes) in the memory
318      [mem]. It returns the new memory and a pointer to the beginning of the
319      allocated area. *)
320  let alloc mem size =
321    alloc2 mem Offset.zero (Offset.of_int size)
322
323
324  let size_of_mq = function
325    | MQ_int8unsigned | MQ_int8signed -> 1
326    | MQ_int16unsigned | MQ_int16signed -> 2
327    | MQ_int32 | MQ_float32 -> 4
328    | MQ_float64 -> 8
329    | MQ_pointer -> D.ptr_size
330    | MQ_chunk -> D.ptr_size/2
331
332  let cast_of_mq = function
333    | MQ_int8unsigned -> Value.cast8unsigned
334    | MQ_int8signed -> Value.cast8signed
335    | MQ_int16unsigned -> Value.cast16unsigned
336    | MQ_int16signed -> Value.cast16signed
337    | MQ_int32 -> Value.cast32
338    | MQ_float32 | MQ_float64 -> error "float not supported."
339    | MQ_pointer | MQ_chunk -> (fun v -> v)
340
341  (* The 'safe'-prefixed functions below raise an error when the argument is not
342     of the expected form. *)
343
344  let safe_to_pointer msg v =
345    if Value.is_pointer v then Value.to_pointer v
346    else error msg
347
348  let safe_find msg find a map =
349    try find a map
350    with Not_found -> error msg
351
352  let safe_find_block msg b mem = safe_find msg BlockMap.find b mem.blocks
353
354  let safe_find_contents msg b mem = match safe_find_block msg b mem with
355    | Contents contents -> contents
356    | Fun_def _ -> error msg
357
358  let safe_find_offset msg off contents =
359    safe_find msg OffsetMap.find off contents.cells
360
361  let memory_find msg mem b off =
362    safe_find_offset msg off (safe_find_contents msg b mem)
363
364  (** [all_are_in_list msg mem b first_off last_off dl] returns [true] iff all
365      the datas found in the block [b] of memory [mem] and between offsets
366      [first_off] (inclusive) and [last_off] (exclusive) are in the list
367      [dl]. *)
368  let all_are_in_list msg mem b first_off last_off dl =
369    let d_eq d d' = match d, d' with
370      | Datum (size, v), Datum (size', v') -> (size = size') && (Value.eq v v')
371      | Cont, Cont -> true
372      | _ -> false in
373    let rec aux d = function
374      | [] -> false
375      | d' :: dl -> (d_eq d d') || (aux d dl) in
376    let dl_mem d = aux d dl in
377    match safe_find_block msg b mem with
378      | Contents contents
379          when (Offset.le contents.low first_off) &&
380            (Offset.le last_off contents.high) ->
381        let rec aux off =
382          if Offset.ge off last_off then true
383          else
384            if OffsetMap.mem off contents.cells then
385              let d = OffsetMap.find off contents.cells in
386              (dl_mem d) && (aux (Offset.succ off))
387            else false
388        in
389        aux first_off
390      | _ -> false
391
392  (** [all_are_undef msg mem b first_off last_off] returns [true] iff all the
393      datas found in the block [b] of memory [mem] and between offsets
394      [first_off] (inclusive) and [last_off] (exclusive) are the undef value. *)
395  let all_are_undef msg mem b first_off last_off =
396    all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef)]
397
398  (** [all_are_undef msg mem b first_off last_off] returns [true] iff all the
399      datas found in the block [b] of memory [mem] and between offsets
400      [first_off] (inclusive) and [last_off] (exclusive) are the undef value or
401      the Cont cell. *)
402  let all_are_undef_or_cont msg mem b first_off last_off =
403    all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef) ; Cont]
404
405  let string_of_alignment = function
406    | None -> "none"
407    | Some alignment -> string_of_int alignment
408
409  (** [write_value msg mem b off size v size'] store the value [v] at the offset
410      [off] of the block [b] in the memory [mem]. [size] is the size of the
411      value [v], and [size'] >= [size] is the number of bytes that are actually
412      written. When [size'] > [size], the undefined value is used to fill the
413      remaining memory cells. *)
414  let write_value msg mem b off size v size' =
415    if not (is_aligned off size) then
416      error "Alignment constraint violated when storing value."
417    else
418      let shift_off n = Offset.add off (Offset.of_int n) in
419      match safe_find_block msg b mem with
420        | Contents contents
421            when (Offset.le contents.low off) &&
422              (Offset.le (shift_off size) contents.high) ->
423          let contents = add_cells contents off (Datum (size, v)) in
424          let contents =
425            write_interval contents (Offset.succ off) (shift_off size) Cont in
426          let contents =
427            write_interval contents (shift_off size) (shift_off size')
428              (Datum (1, Value.undef)) in
429          let blocks = BlockMap.add b (Contents contents) mem.blocks in
430          { mem with blocks = blocks }
431        | _ -> error msg
432
433
434  (* Memory free *)
435
436  let free mem addr =
437    if Value.is_pointer addr then
438      let (b, _) = Value.to_pointer addr in
439      { mem with blocks = BlockMap.remove b mem.blocks }
440    else error "free: invalid memory address."
441
442
443  (* Memory load and store *)
444
445  (** [load2 mem size addr] reads a value of size [size] at the address [addr]
446      in memory [mem]. *)
447  let load2 mem size addr =
448    let msg = ("load: invalid memory access. ("^(Value.to_string addr)^")") in
449    let (b, off) = safe_to_pointer msg addr in
450    if not (is_aligned off size) then
451      error "Alignment constraint violated when loading value."
452    else
453      match memory_find msg mem b off with
454        | Datum (size', v) when size <= size' -> 
455          v
456              (*print_string ("Db: load m "^(string_of_memory_q chunk)^" "
457                            ^(Value.to_string addr)^" "^(Value.to_string r)^" ("
458                            ^(Value.to_string v)^")\n"); *)
459        | _ -> print mem;error msg
460
461  (** [load mem chunk addr] reads a value of type [chunk] at the address [addr]
462      in memory [mem]. *)
463  let load mem chunk addr =
464    let size = size_of_mq chunk in
465    cast_of_mq chunk (load2 mem size addr)
466
467
468  (** [write_undef_before msg mem b off] replaces with undefined values the
469      value whose last cell is at offset [off] of block [b] in memory
470      [mem]. *)
471  let write_undef_before msg mem b off =
472    let contents = safe_find_contents msg b mem in
473    let d = Datum (1, Value.undef) in
474    let rec aux off contents =
475      if OffsetMap.mem off contents.cells then
476        let contents' = add_cells contents off d in
477        match OffsetMap.find off contents.cells with
478          | Datum _ -> contents'
479          | Cont -> aux (Offset.pred off) contents'
480      else contents
481    in
482    let contents = aux off contents in
483    { mem with blocks = BlockMap.add b (Contents contents) mem.blocks }
484
485  (** [store2 mem size addr v] writes the value [v] of size [size] at address
486      [addr] in memory [mem]. *)
487  let store2 mem size addr v =
488    let msg = "store: invalid memory access." in
489    let (b, off) = safe_to_pointer msg addr in
490    let shift_off n = Offset.add off (Offset.of_int n) in
491    (*print_string ("Db: store m "^(string_of_memory_q chunk)^" "
492      ^(Value.to_string addr)^" "^(Value.to_string v)^" ("
493      ^(Value.to_string v0)^")\n"); *)
494    match memory_find msg mem b off with
495      | Datum (size', _) when size <= size' ->
496          write_value msg mem b off size v size'
497      | Datum (size', _)
498          when all_are_undef msg mem b (shift_off size') (shift_off size) ->
499          write_value msg mem b off size v size'
500      | Cont when all_are_undef_or_cont msg mem b off (shift_off size) ->
501          let mem = write_value msg mem b off size v size in 
502          write_undef_before msg mem b (Offset.pred off)
503      | _ -> error msg
504
505  (** [store mem chunk addr v] writes the value [v] interpreted as a value of
506      type [chunk] at address [addr] in memory [mem]. *)
507  let store mem chunk addr v =
508    store2 mem (size_of_mq chunk) addr (cast_of_mq chunk v)
509
510
511(* Data manipulation *)
512
513  let value_of_data = function
514    | AST.Data_reserve _ -> Value.undef
515    | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i -> Value.of_int i
516    | AST.Data_float32 f | AST.Data_float64 f -> Value.of_float f
517
518  let size_of_data = function
519    | AST.Data_reserve n -> n
520    | data -> size_of_mq (mq_of_data data)
521
522  let offsets_size_of_datas datas =
523    align Offset.zero (List.map size_of_data datas)
524
525  (** [alloc_datas mem datas] returns the memory and the address obtained by
526      allocating space and storing the datas [datas] in the memory [mem]. *)
527  let alloc_datas mem datas =
528    let (offs_of_datas, size) = offsets_size_of_datas datas in
529    let (mem, addr) = alloc mem size in
530    let shift_addr off = Value.add addr (Value.of_int_repr off) in
531    let f mem data off = match data with
532      | AST.Data_reserve _ -> mem
533      | _ -> store mem (mq_of_data data) (shift_addr off) (value_of_data data)
534    in
535    (List.fold_left2 f mem datas offs_of_datas, addr)
536
537  let size_of_datas datas = snd (offsets_size_of_datas datas)
538
539  (** [offsets_of_datas datas] returns the aligned offsets for the datas
540      [datas], starting at offset 0. *)
541  let offsets_of_datas datas =
542    let (offs_of_datas, _) = offsets_size_of_datas datas in
543    List.combine datas (List.map Offset.to_int offs_of_datas)
544
545  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
546      of size [sizes]. *)
547  let align off sizes =
548    let (offsets, size) = align (Offset.of_int off) sizes in
549    (List.map Offset.to_int offsets, size)
550
551
552  (* Global environment manipulation *)
553
554  (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
555      memory [mem], and associates the global variable [x] with the address of
556      the block. *)
557  let add_var mem v_id datas =
558    let (mem, addr) = alloc_datas mem datas in
559    let addr_of_global = GlobalMap.add v_id addr mem.addr_of_global in
560    { mem with addr_of_global = addr_of_global }
561
562  (** [add_fun_def mem f def] stores the function definition [def] in a new
563      block of memory [mem], and associates the function name [f] with the
564      address of the block. *)
565  let add_fun_def mem f_id f_def =
566    let b = mem.next_fun_block in
567    let next_fun_block = Block.pred mem.next_fun_block in
568    let addr = Value.of_pointer (b, Offset.zero) in
569    let addr_of_global = GlobalMap.add f_id addr mem.addr_of_global in
570    let blocks = BlockMap.add b (Fun_def f_def) mem.blocks in
571    { mem with blocks = blocks ;
572               addr_of_global = addr_of_global ;
573               next_fun_block = next_fun_block }
574
575  (** [find_global mem x] returns the address associated with the global symbol
576      [x] in memory [mem]. [x] may be a global variable or the name of a
577      function. *)
578  let find_global mem gid =
579    if GlobalMap.mem gid mem.addr_of_global then
580      GlobalMap.find gid mem.addr_of_global
581    else error ("Unknown global \"" ^ gid ^ "\"")
582
583  (** [find_fun_def mem addr] returns the function definition found at address
584      [addr] in memory [mem]. Raises an error if no function definition is
585      found. *)
586  let find_fun_def mem v =
587    let msg = "Invalid access to a function definition." in
588    let (b, _) = safe_to_pointer msg v in
589    match safe_find_block msg b mem with
590      | Contents _ -> error msg
591      | Fun_def def -> def
592
593
594 
595
596end
Note: See TracBrowser for help on using the repository browser.