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

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

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 16.5 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
6(** In the module, every size is expressed in bytes. *)
7
8
9let error_prefix = "Memory"
10let error s = Error.global_error error_prefix s
11
12
13(** Memory quantities is the size and type of what can be loaded or stored in
14    memory. *)
15
16type quantity =
17  | QInt of int (* Sized integer *)
18  | QPtr        (* Pointer *)
19
20let string_of_quantity = function
21  | QInt i -> string_of_int i
22  | QPtr -> "ptr"
23
24
25let size_of_data = function
26  | AST.Data_reserve n -> n
27  | AST.Data_int8 _ -> 1
28  | AST.Data_int16 _ -> 2
29  | AST.Data_int32 _ -> 4
30  | AST.Data_float32 _ -> 4
31  | AST.Data_float64 _ -> 8
32
33
34(** This is the signature of the parameter module of the functor. *)
35
36module type DATA_SIZE =
37sig
38  val int_size  : int
39  val ptr_size  : int
40  val alignment : int option
41end
42
43
44(** This is the signature of the module that provides functions and types to
45    manipulate memories. *)
46
47module type S =
48sig
49
50  val int_size  : int
51  val ptr_size  : int
52  val alignment : int option
53
54  val size_of_quantity : quantity -> int
55
56  module Value : Value.S
57
58  (* Memory. A memory contains values and function definitions. Since the memory
59     module will be used by the interpreters of the various languages of the
60     compilation chain, the type of memory is polymorphic with the type of
61     function definitions. *)
62
63  type 'fun_def memory
64
65  (* Memory manipulation *)
66
67  val empty : 'fun_def memory
68
69  (** [alloc mem size] allocates a block of [size] bytes in the memory [mem]. It
70      returns the new memory and the address of the beginning of the newly
71      allocated area. *)
72  val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.address
73
74  (* Memory free *)
75
76  val free : 'fun_def memory -> Value.address -> 'fun_def memory
77
78  (* Memory load and store *)
79
80  (** [load mem size addr] reads [size] bytes from address [addr] in memory
81      [mem] and returns the value found. *)
82  val load : 'fun_def memory -> int -> Value.address -> Value.t
83  val loadq : 'fun_def memory -> quantity -> Value.address -> Value.t
84
85  (** [store mem size addr v] writes the [size] first bytes (little endian
86      representation) of value [v] at address [addr] in memory [mem]. *)
87  val store  : 'fun_def memory -> int -> Value.address -> Value.t ->
88               'fun_def memory
89  val storeq : 'fun_def memory -> quantity -> Value.address -> Value.t ->
90               'fun_def memory
91
92  (* Globals management *)
93
94  (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
95      memory [mem], and associates the global variable [x] with the address of
96      the block. *)
97  val add_var : 'fun_def memory -> AST.ident -> AST.data list -> 'fun_def memory
98
99  (** [add_fun_def mem f def] stores the function definition [def] in a new
100      block of memory [mem], and associates the function name [f] with the
101      address of the block. *)
102  val add_fun_def : 'fun_def memory -> AST.ident -> 'fun_def -> 'fun_def memory
103
104  val mem_global : 'fun_def memory -> AST.ident -> bool
105
106  (** [find_global mem x] returns the address associated with the global symbol
107      [x] in memory [mem]. [x] may be a global variable or the name of a
108      function. *)
109  val find_global : 'fun_def memory -> AST.ident -> Value.address
110
111  (** [find_fun_def mem addr] returns the function definition found at address
112      [addr] in memory [mem]. Raises an error if no function definition is
113      found. *)
114  val find_fun_def : 'fun_def memory -> Value.address -> 'fun_def
115
116  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
117      of size [sizes]. *)
118  val align : int (* starting offset *) -> int list (* sizes *) ->
119              (int list (* resulting offsets *) * int (* full size *))
120
121  val size_of_datas : AST.data list -> int
122
123  (** [offsets_of_datas datas] returns the aligned offsets for the datas
124      [datas], starting at offset 0. *)
125  val offsets_of_datas : AST.data list -> (AST.data * int (* offset *)) list
126
127  val alloc_datas : 'fun_def memory -> AST.data list ->
128                    ('fun_def memory * Value.address)
129
130  val to_string : 'fun_def memory -> string
131  val print : 'fun_def memory -> unit
132
133end
134
135
136(** The functor of a memory module. *)
137
138module Make (D : DATA_SIZE) =
139struct
140
141  module Value = Value.Make (D)
142  module Block = Value.Block
143  module Offset = Value.Offset
144
145  let address_of_block_offset b off =
146    Value.of_mem_address (Value.make_mem_address b off)
147
148  let int_size = D.int_size
149  let ptr_size = D.ptr_size
150  let alignment = D.alignment
151
152  let size_of_quantity = function
153    | QInt i -> i
154    | QPtr -> ptr_size
155
156
157  module OffsetMap = Map.Make (Offset)
158  type offsetMap = Value.chunk OffsetMap.t
159  type offset = Offset.t
160
161  (* Empty cells are interpreted as an undefined byte value. *)
162
163  type contents =
164      { low   : offset ; (* inclusive *)
165        high  : offset ; (* inclusive *)
166        cells : offsetMap }
167
168  let update_cells contents cells = { contents with cells = cells }
169  let add_cells contents off v =
170    update_cells contents (OffsetMap.add off v contents.cells)
171  let remove_cells contents off =
172    update_cells contents (OffsetMap.remove off contents.cells)
173
174  (* Alignment *)
175
176  let is_multiple n m = m mod n = 0
177
178  (** [align off size] returns the offset greater or equal to [off] that is
179      aligned for storing a value of size [size]. *)
180  let align off size = match D.alignment with
181    | None -> off
182    | Some alignment when (size <= alignment) && (is_multiple size alignment) ->
183      let size = Offset.of_int size in
184      let rem = Offset.modulou off size in
185      if Offset.eq rem Offset.zero then off
186      else Offset.add off (Offset.sub size rem)
187    | Some alignment ->
188      let size = Offset.of_int alignment in
189      let rem = Offset.modulou off size in
190      if Offset.eq rem Offset.zero then off
191      else Offset.add off (Offset.sub size rem)
192
193  let is_aligned off size = Offset.eq off (align off size)
194
195  (** [pad off] returns the offset that is obtained by adding some padding from
196      [off] and such that the result is aligned. *)
197  let pad off = match D.alignment with
198    | None -> off
199    | Some alignment -> align off alignment
200
201  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
202      of size [sizes]. *)
203  let align off sizes =
204    let rec aux (acc_offs, acc_size) off = function
205      | [] ->
206        let end_off = pad off in
207        let added_size = Offset.sub end_off off in
208        let added_size = Offset.to_int added_size in
209        (acc_offs, acc_size + added_size)
210      | size :: sizes ->
211        let aligned_off = align off size in
212        let next_off = Offset.add aligned_off (Offset.of_int size) in
213        let added_size = Offset.sub next_off off in
214        let added_size = Offset.to_int added_size in
215        let acc = (acc_offs @ [aligned_off], acc_size + added_size) in
216        aux acc next_off sizes
217    in
218    aux ([], 0) off sizes
219
220
221  (* Contents in memory. The type of function definitions varies from a language
222     to another; thus, it is left generic. *)
223
224  type 'fun_def content =
225    | Contents of contents
226    | Fun_def of 'fun_def
227
228
229  (* The mapping from blocks to contents. *)
230
231  module BlockMap = Map.Make (Block)
232  type 'fun_def blockMap = 'fun_def content BlockMap.t
233  type block = Block.t
234
235  (* The mapping from global identifiers to blocks (negative for function
236     definitions and positive for global variables). *)
237
238  module GlobalMap = Map.Make (String)
239  type globalMap = Value.address GlobalMap.t
240
241  (* The memory.
242     It is a mapping from blocks to contents, a mapping from global identifiers
243     (variables and functions) to pointers, a mapping from (negative) blocks to
244     function definition, the next free positive block and the next free
245     negative block. *)
246
247  type 'fun_def memory =
248      { blocks           : 'fun_def blockMap ;
249        addr_of_global   : globalMap ;
250        next_block       : block ;
251        next_fun_block   : block }
252
253  (* Pretty printing *)
254
255  let to_string mem =
256    let i = ref 0 in
257    let string_of_cell off v s =
258      let s' = if !i mod 4 = 0 then (i := 0 ; "\n ") else "" in
259      i := !i+1 ;
260      let sv =
261        if Value.is_undef_byte v then ""
262        else Printf.sprintf "[%s]: %s"
263          (Offset.to_string off) (Value.string_of_chunk v) in
264      Printf.sprintf "%s%s %s" s s' sv in
265    let string_of_cells cells = OffsetMap.fold string_of_cell cells "" in
266    let string_of_block b content s =
267      (Printf.sprintf "%s\nBlock %s: " s (Block.to_string b)) ^
268      (match content with
269        | Contents contents ->
270          i := 0 ;
271          Printf.sprintf "(%s -> %s)%s"
272            (Offset.to_string contents.low)
273            (Offset.to_string contents.high)
274            (string_of_cells contents.cells)
275        | Fun_def _ -> "function definition") in 
276    Printf.sprintf "%s\n" (BlockMap.fold string_of_block mem.blocks "")
277
278    let print mem = Printf.printf "%s%!" (to_string mem)
279
280
281  (* Memory manipulation *)
282
283  let empty =
284    { blocks = BlockMap.empty ;
285      addr_of_global = GlobalMap.empty ;
286      next_block = Block.of_int 1 ;
287      next_fun_block = Block.of_int (-1) }
288
289  (* Memory allocation *)
290
291  (** [alloc2 mem low high] allocates in memory [mem] a new block whose readable
292      and writable offsets are the interval [low] (inclusive) [high]
293      (inclusive). *)
294  let alloc2 mem low high =
295    let b = mem.next_block in
296    let contents = { low = low ; high = high ; cells = OffsetMap.empty } in
297    let blocks = BlockMap.add b (Contents contents) mem.blocks in
298    let next_block = Block.succ mem.next_block in
299    let mem' = { mem with blocks = blocks ; next_block = next_block } in
300    (mem', address_of_block_offset b low)
301
302  (** [alloc mem size] allocates a block of [size] bytes in the memory [mem]. It
303      returns the new memory and the address of the beginning of the newly
304      allocated area. *)
305  let alloc mem size =
306    if size = 0 then (mem, Value.null)
307    else alloc2 mem Offset.zero (Offset.of_int (size-1))
308
309
310  (* The 'safe'-prefixed functions below raise an error when the argument is not
311     of the expected form. *)
312
313  let safe_to_address msg vs = 
314    if Value.is_mem_address vs then Value.to_mem_address vs
315    else error msg
316
317  let safe_find not_found find a map =
318    try find a map
319    with Not_found -> not_found ()
320
321  let safe_find_err msg = safe_find (fun () -> error msg)
322
323  let safe_find_block msg b mem = safe_find_err msg BlockMap.find b mem.blocks
324
325  let safe_find_contents msg b mem = match safe_find_block msg b mem with
326    | Contents contents -> contents
327    | Fun_def _ -> error msg
328
329  let safe_find_offset msg off contents =
330    if (Offset.leu contents.low off) && (Offset.leu off contents.high) then
331      safe_find (fun () -> Value.undef_byte) OffsetMap.find off contents.cells
332    else error msg
333
334  let memory_find msg mem b off =
335    safe_find_offset msg off (safe_find_contents msg b mem)
336
337
338  (* Memory free *)
339
340  let free mem vs =
341    let addr = safe_to_address "free: invalid memory address." vs in
342    let (b, _) = Value.decompose_mem_address addr in
343    { mem with blocks = BlockMap.remove b mem.blocks }
344
345
346  (* Memory load *)
347
348  (** [load_bytes msg mem b off size] reads [size] bytes from the block [b] and
349      offset [off] in memory [mem] and returns the value found. If an error
350      occurs, [msg] will be printed. *)
351  let load_bytes msg mem b off size =
352    let shift_off n = Offset.add off (Offset.of_int n) in
353    let rec aux n =
354      if n >= size then []
355      else (memory_find msg mem b (shift_off n)) :: (aux (n+1)) in
356    Value.merge (aux 0)
357
358  (** [load mem size addr] reads [size] bytes from address [addr] in memory
359      [mem] and returns the value found. *)
360  let load mem size vs =
361    let msg = "load: invalid memory access." in
362    let addr = safe_to_address msg vs in
363    let (b, off) = Value.decompose_mem_address addr in
364    if not (is_aligned off size) then
365      error "Alignment constraint violated when loading value."
366    else load_bytes msg mem b off size
367
368  let loadq mem q vs = load mem (size_of_quantity q) vs
369
370
371  (* Memory store *)
372
373  (** [store_chunks msg mem size b off chunks] writes the [size] first chunks of
374      list [chunks] at the offset [off] of the block [b] in the memory [mem]. *)
375  let store_chunks msg mem size b off chunks =
376    let shift_off n = Offset.add off (Offset.of_int n) in
377    let f i contents chunk =
378      let off' = shift_off i in
379      if (Offset.leu contents.low off') &&
380         (Offset.leu off' contents.high) then
381        if Value.is_undef_byte chunk then contents
382        else add_cells contents off' chunk
383      else error msg in
384    match safe_find_block msg b mem with
385      | Contents contents ->
386        let contents = MiscPottier.foldi_until size f contents chunks in
387        let blocks = BlockMap.add b (Contents contents) mem.blocks in
388        { mem with blocks = blocks }
389      | _ -> error msg
390
391  (** [store mem size addr v] writes the [size] first bytes (little endian
392      representation) of value [v] at address [addr] in memory [mem]. *)
393  let store mem size vs v =
394    let msg = "store: invalid memory access." in
395    let addr = safe_to_address msg vs in
396    let (b, off) = Value.decompose_mem_address addr in
397    if not (is_aligned off size) then
398      error "Alignment constraint violated when storing value."
399    else store_chunks msg mem size b off (Value.break v)
400
401  let storeq mem q vs v = store mem (size_of_quantity q) vs v
402
403
404  (* Data manipulation *)
405
406  let value_of_data = function
407    | AST.Data_reserve _ -> Value.undef
408    | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i -> Value.of_int i
409    | AST.Data_float32 f | AST.Data_float64 f -> error "float not supported."
410
411  let offsets_size_of_datas datas =
412    align Offset.zero (List.map size_of_data datas)
413
414  (** [alloc_datas mem datas] returns the memory and the address obtained by
415      allocating space and storing the datas [datas] in the memory [mem]. *)
416  let alloc_datas mem datas =
417    let msg = "cannot allocate datas." (* TODO *) in
418    let (offs_of_datas, size) = offsets_size_of_datas datas in
419    let (mem, vs) = alloc mem size in
420    let addr = safe_to_address msg vs in
421    let (b, off) = Value.decompose_mem_address addr in
422    let shift_addr off' =
423      let off = Offset.add off off' in
424      address_of_block_offset b off in
425    let f mem data off = match data with
426      | AST.Data_reserve _ -> mem
427      | _ -> store mem (size_of_data data) (shift_addr off) (value_of_data data)
428    in
429    (List.fold_left2 f mem datas offs_of_datas, vs)
430
431  let size_of_datas datas = snd (offsets_size_of_datas datas)
432
433  (** [offsets_of_datas datas] returns the aligned offsets for the datas
434      [datas], starting at offset 0. *)
435  let offsets_of_datas datas =
436    let (offs_of_datas, _) = offsets_size_of_datas datas in
437    List.combine datas (List.map Offset.to_int offs_of_datas)
438
439  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
440      of size [sizes]. *)
441  let align off sizes =
442    let (offsets, size) = align (Offset.of_int off) sizes in
443    (List.map Offset.to_int offsets, size)
444
445
446  (* Globals manipulation *)
447
448  (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
449      memory [mem], and associates the global variable [x] with the address of
450      the block. *)
451  let add_var mem v_id datas =
452    let (mem, vs) = alloc_datas mem datas in
453    let addr_of_global = GlobalMap.add v_id vs mem.addr_of_global in
454    { mem with addr_of_global = addr_of_global }
455
456  (** [add_fun_def mem f def] stores the function definition [def] in a new
457      block of memory [mem], and associates the function name [f] with the
458      address of the block. *)
459  let add_fun_def mem f_id f_def =
460    let b = mem.next_fun_block in
461    let next_fun_block = Block.pred mem.next_fun_block in
462    let vs = address_of_block_offset b Offset.zero in
463    let addr_of_global = GlobalMap.add f_id vs mem.addr_of_global in
464    let blocks = BlockMap.add b (Fun_def f_def) mem.blocks in
465    { mem with blocks = blocks ;
466               addr_of_global = addr_of_global ;
467               next_fun_block = next_fun_block }
468
469  let mem_global mem id = GlobalMap.mem id mem.addr_of_global
470
471  (** [find_global mem x] returns the address associated with the global symbol
472      [x] in memory [mem]. [x] may be a global variable or the name of a
473      function. *)
474  let find_global mem gid =
475    if GlobalMap.mem gid mem.addr_of_global then
476      GlobalMap.find gid mem.addr_of_global
477    else error ("Unknown global \"" ^ gid ^ "\"")
478
479  (** [find_fun_def mem addr] returns the function definition found at address
480      [addr] in memory [mem]. Raises an error if no function definition is
481      found. *)
482  let find_fun_def mem vs =
483    let msg = "Invalid access to a function definition." in
484    let (b, _) = Value.decompose_mem_address (safe_to_address msg vs) in
485    match safe_find_block msg b mem with
486      | Contents _ -> error msg
487      | Fun_def def -> def
488
489end
Note: See TracBrowser for help on using the repository browser.