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

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