src/common/memory.ml

   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
   9 let error_prefix = "Memory"
  10 let error s = Error.global_error error_prefix s
  11
  12
  13 let string_of_quantity = function
  14   | AST.QInt i -> "int" ^ (string_of_int (i*8))
  15   | AST.QOffset -> "offset"
  16   | AST.QPtr -> "ptr"
  17
  18
  19 let 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
  30 let 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
  48 module type DATA_SIZE =
  49 sig
  50   val int_size  : int
  51   val ptr_size  : int
  52   val alignment : int option
  53 end
  54
  55
  56 (** This is the signature of the module that provides functions and types to
  57     manipulate memories. *)
  58
  59 module type S =
  60 sig
  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
 158 end
 159
 160
 161 (** The functor of a memory module. *)
 162
 163 module Make (D : DATA_SIZE) =
 164 struct
 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
 548 end