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. *)
6 (** In the module, every size is expressed in bytes. *)
9 let error_prefix = "Memory"
10 let error s = Error.global_error error_prefix s
13 let string_of_quantity = function
14 | AST.QInt i -> "int" ^ (string_of_int (i*8))
15 | AST.QOffset -> "offset"
19 let size_of_data = function
21 | AST.Data_reserve n -> n
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
30 let rec all_offsets size = match size with
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
42 else (f i) @ (aux (i+1)) in
46 (** This is the signature of the parameter module of the functor. *)
48 module type DATA_SIZE =
52 val alignment : int option
56 (** This is the signature of the module that provides functions and types to
57 manipulate memories. *)
64 val alignment : int option
66 val size_of_quantity : AST.quantity -> int
68 module Value : Value.S
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. *)
77 (* Memory manipulation *)
79 val empty : 'fun_def memory
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
84 val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.address
88 val free : 'fun_def memory -> Value.address -> 'fun_def memory
90 (* Memory load and store *)
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
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 ->
101 val storeq : 'fun_def memory -> AST.quantity -> Value.address -> Value.t ->
104 (* Globals management *)
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. *)
110 'fun_def memory -> AST.ident -> AST.abstract_size -> AST.data list option ->
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
118 val mem_global : 'fun_def memory -> AST.ident -> bool
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
123 val find_global : 'fun_def memory -> AST.ident -> Value.address
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
128 val find_fun_def : 'fun_def memory -> Value.address -> 'fun_def
131 (** [align off size] returns the aligned offsets (starting at [off]) of datas
133 val align : int (* starting offset *) -> AST.abstract_size (* sizes *) ->
134 (int list (* resulting offsets *) * int (* full size *))
136 val concrete_offsets_size : AST.abstract_size -> int list * int
138 val concrete_offsets : AST.abstract_size -> int list
140 val concrete_size : AST.abstract_size -> int
142 val concrete_offset : AST.abstract_offset -> int
145 val size_of_datas : AST.data list -> int
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
151 val alloc_datas : 'fun_def memory -> AST.data list ->
152 ('fun_def memory * Value.address)
155 val to_string : 'fun_def memory -> string
156 val print : 'fun_def memory -> unit
161 (** The functor of a memory module. *)
163 module Make (D : DATA_SIZE) =
166 module Value = Value.Make (D)
167 module Block = Value.Block
168 module Offset = Value.Offset
170 let address_of_block_offset b off =
171 Value.of_mem_address (Value.make_mem_address b off)
173 let int_size = D.int_size
174 let ptr_size = D.ptr_size
175 let alignment = D.alignment
177 let size_of_quantity = function
179 | AST.QOffset -> int_size
180 | AST.QPtr -> ptr_size
183 module OffsetMap = Map.Make (Offset)
184 type offsetMap = Value.chunk OffsetMap.t
185 type offset = Offset.t
187 (* Empty cells are interpreted as an undefined byte value. *)
190 { low : offset ; (* inclusive *)
191 high : offset ; (* inclusive *)
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)
202 let is_multiple n m = m mod n = 0
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
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)
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)
219 let is_aligned off size = Offset.eq off (align_off off size)
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
225 | Some alignment -> align_off off alignment
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)))
234 (* Contents in memory. The type of function definitions varies from a language
235 to another; thus, it is left generic. *)
237 type 'fun_def content =
238 | Contents of contents
239 | Fun_def of 'fun_def
242 (* The mapping from blocks to contents. *)
244 module BlockMap = Map.Make (Block)
245 type 'fun_def blockMap = 'fun_def content BlockMap.t
248 (* The mapping from global identifiers to blocks (negative for function
249 definitions and positive for global variables). *)
251 module GlobalMap = Map.Make (String)
252 type globalMap = Value.address GlobalMap.t
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
260 type 'fun_def memory =
261 { blocks : 'fun_def blockMap ;
262 addr_of_global : globalMap ;
264 next_fun_block : block }
266 (* Pretty printing *)
270 let string_of_cell off v s =
271 let s' = if !i mod 4 = 0 then (i := 0 ; "\n ") else "" in
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)) ^
282 | Contents contents ->
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 "")
291 let print mem = Printf.printf "%s%!" (to_string mem)
294 (* Memory manipulation *)
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) }
302 (* Memory allocation *)
304 (** [alloc2 mem low high] allocates in memory [mem] a new block whose readable
305 and writable offsets are the interval [low] (inclusive) [high]
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)
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
319 if size = 0 then (mem, Value.null)
320 else alloc2 mem Offset.zero (Offset.of_int (size-1))
323 (* The 'safe'-prefixed functions below raise an error when the argument is not
324 of the expected form. *)
326 let safe_to_address msg vs =
327 if Value.is_mem_address vs then Value.to_mem_address vs
330 let safe_find not_found find a map =
332 with Not_found -> not_found ()
334 let safe_find_err msg = safe_find (fun () -> error msg)
336 let safe_find_block msg b mem = safe_find_err msg BlockMap.find b mem.blocks
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
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
347 let memory_find msg mem b off =
348 safe_find_offset msg off (safe_find_contents msg b mem)
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 }
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
368 else (memory_find msg mem b (shift_off n)) :: (aux (n+1)) in
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
381 let loadq mem q vs = load mem (size_of_quantity q) vs
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
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 }
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)
414 let storeq mem q vs v = store mem (size_of_quantity q) vs v
417 (* Data manipulation *)
419 let value_of_data = function
421 | AST.Data_reserve _ -> Value.undef
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."
428 | C of concrete_size list
430 let rec first_offset = function
432 | C [] -> raise (Failure "Memory.first_offset")
433 | C (csize :: _) -> first_offset csize
435 let first_offsets = function
437 | C sizes -> List.map first_offset sizes
439 let rec all_offsets = function
441 | C sizes -> List.flatten (List.map all_offsets sizes)
443 let rec full_align off = function
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)
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
463 let start_off = pad off in
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)
471 | AST.SArray (n, size) ->
472 let sizes = MiscPottier.make size n in
473 full_align off (AST.SProd sizes)
476 let (offsets, full_size) = full_align (Offset.of_int off) size in
477 (List.map Offset.to_int (first_offsets offsets), full_size)
479 let concrete_offsets_size = align 0
481 let concrete_offsets size = fst (concrete_offsets_size size)
483 let concrete_size size = snd (concrete_offsets_size size)
485 let concrete_offset (size, depth) =
486 let offsets = concrete_offsets size in
487 List.nth offsets depth
490 (* Globals manipulation *)
492 let store_datas_opt mem addr offsets = function
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?)."
502 let offset_datas = List.combine offsets datas in
503 List.fold_left f mem offset_datas
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 }
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 }
528 let mem_global mem id = GlobalMap.mem id mem.addr_of_global
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
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 ^ "\"")
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
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