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

(** This file gives a memory model that can be used by the interpreter
    of various languages throughout the compilation process and
    following the memory model of the CompCert compiler. *)

open IntValue


let error_prefix = "Memory"
let error s = Error.global_error error_prefix s


(* Memory quantities are the size and the type of what can be loaded
   and stored in memory *)

type memory_q =
  | MQ_int8signed | MQ_int8unsigned | MQ_int16signed | MQ_int16unsigned
  | MQ_int32 | MQ_float32 | MQ_float64 | MQ_pointer | MQ_chunk

let string_of_memory_q = function
  | MQ_int8signed -> "int8s"
  | MQ_int8unsigned -> "int8u"
  | MQ_int16signed -> "int16s"
  | MQ_int16unsigned -> "int16u"
  | MQ_int32 -> "int32"
  | MQ_float32 -> "float"
  | MQ_float64 -> "float64"
  | MQ_pointer -> "ptr"
  | MQ_chunk -> "chunk"

let mq_of_data = function
  | AST.Data_reserve _ -> assert false (* Should not be called on this *)
  | AST.Data_int8 _ -> MQ_int8signed
  | AST.Data_int16 _ -> MQ_int16signed
  | AST.Data_int32 _ -> MQ_int32
  | AST.Data_float32 _ -> MQ_float32
  | AST.Data_float64 _ -> MQ_float64

let type_of_memory_q = function
  | MQ_int8signed | MQ_int8unsigned | MQ_int16signed | MQ_int16unsigned
  | MQ_int32 -> AST.Sig_int
  | MQ_float32 | MQ_float64 -> AST.Sig_float
  | MQ_pointer -> AST.Sig_ptr
  | MQ_chunk -> error "Trying to get the type of a pointer chunk."


(** This is the signature of the parameter module of the functor. *)

module type DATA_SIZE =
sig
  val int_size  : int
  val ptr_size  : int
  val alignment : int option
end


(** This is the signature of the module that provides functions and types to
    manipulate memories. *)

module type S =
sig

  val mq_of_ptr : memory_q
  val int_size  : int
  val ptr_size  : int
  val alignment : int option

  module Value : Value.S

  (* Memory. A memory contains values and function definitions. Since the memory
     module will be used by the interpreters of the various languages of the
     compilation chain, the type of memory is polymorphic with the type of
     function definitions. *)

  type 'fun_def memory

  (* Memory manipulation *)

  val empty : 'fun_def memory

  (** [alloc mem size] allocates a block of [size] size (in bytes) in the memory
      [mem]. It returns the new memory and a pointer to the beginning of the
      allocated area. *)
  val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.t

  (* Memory free *)

  val free : 'fun_def memory -> Value.t -> 'fun_def memory

  (* Memory load and store *)

  (** [load mem chunk addr] reads a value of type [chunk] at the address [addr]
      in memory [mem]. *)
  val load : 'fun_def memory -> memory_q -> Value.t -> Value.t
  (** [load2 mem size addr] reads a value of size [size] at the address [addr]
      in memory [mem]. *)
  val load2 : 'fun_def memory -> int -> Value.t -> Value.t

  (** [store mem chunk addr v] writes the value [v] interpreted as a value of
      type [chunk] at address [addr] in memory [mem]. *)
  val store  : 'fun_def memory -> memory_q -> Value.t -> Value.t ->
               'fun_def memory
  (** [store mem size addr v] writes the value [v] of size [size] at address
      [addr] in memory [mem]. *)
  val store2 : 'fun_def memory -> int -> Value.t -> Value.t ->
               'fun_def memory

  (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
      memory [mem], and associates the global variable [x] with the address of
      the block. *)
  val add_var : 'fun_def memory -> AST.ident -> AST.data list -> 'fun_def memory

  (** [add_fun_def mem f def] stores the function definition [def] in a new
      block of memory [mem], and associates the function name [f] with the
      address of the block. *)
  val add_fun_def : 'fun_def memory -> AST.ident -> 'fun_def -> 'fun_def memory

  (** [find_global mem x] returns the address associated with the global symbol
      [x] in memory [mem]. [x] may be a global variable or the name of a
      function. *)
  val find_global : 'fun_def memory -> AST.ident -> Value.t

  (** [find_fun_def mem addr] returns the function definition found at address
      [addr] in memory [mem]. Raises an error if no function definition is
      found. *)
  val find_fun_def : 'fun_def memory -> Value.t -> 'fun_def

  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
      of size [sizes]. *)
  val align : int (* starting offset *) -> int list (* sizes *) ->
              (int list (* resulting offsets *) * int (* full size *))

  val size_of_datas    : AST.data list -> int

  (** [offsets_of_datas datas] returns the aligned offsets for the datas
      [datas], starting at offset 0. *)
  val offsets_of_datas : AST.data list -> (AST.data * int (* offset *)) list

  val alloc_datas      : 'fun_def memory -> AST.data list ->
                         ('fun_def memory * Value.t)

  val print : 'fun_def memory -> unit

end


(** The functor to a memory module. *)

module Make (D : DATA_SIZE) =
struct

  module Value = Value.Make (D)
  module Block = Value.Block
  module Offset = Value.Offset

  let mq_of_ptr = MQ_pointer

  let int_size = D.int_size
  let ptr_size = D.ptr_size
  let alignment = D.alignment


  (* Contents of a variable. *)

  type cell =
    | Datum of int * Value.t (* the size of the content and its value *)
    | Cont                   (* the continuation of a content defined in a
                                previous block *)


  module OffsetMap = Map.Make (Offset)
  type offsetMap = cell OffsetMap.t
  type offset = Offset.t

  type contents =
      { low   : offset ;
        high  : offset ;
        cells : offsetMap }

  let update_cells contents cells = { contents with cells = cells }
  let add_cells contents off v =
    update_cells contents (OffsetMap.add off v contents.cells)

  (* Alignment *)

  let is_multiple n m = m mod n = 0

  (** [align off size] returns the offset greater or equal to [off] that is
      aligned for storing a value of size [size]. *)
  let align off size = match D.alignment with
    | None -> off
    | Some alignment when (size <= alignment) && (is_multiple size alignment) ->
      let size = Offset.of_int size in
      let rem = Offset.modulou off size in
      if Offset.eq rem Offset.zero then off
      else Offset.add off (Offset.sub size rem)
    | Some alignment ->
      let size = Offset.of_int alignment in
      let rem = Offset.modulou off size in
      if Offset.eq rem Offset.zero then off
      else Offset.add off (Offset.sub size rem)

  let is_aligned off size = Offset.eq off (align off size)

  (** [pad off] returns the offset that is obtained by adding some padding from
      [off] and such that the result is aligned. *)
  let pad off = match D.alignment with
    | None -> off
    | Some alignment -> align off alignment

  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
      of size [sizes]. *)
  let align off sizes =
    let rec aux (acc_offs, acc_size) off = function
      | [] ->
        let end_off = pad off in
        let added_size = Offset.sub end_off off in
        let added_size = Offset.to_int added_size in
        (acc_offs, acc_size + added_size)
      | size :: sizes ->
        let aligned_off = align off size in
        let next_off = Offset.add aligned_off (Offset.of_int size) in
        let added_size = Offset.sub next_off off in
        let added_size = Offset.to_int added_size in
        let acc = (acc_offs @ [aligned_off], acc_size + added_size) in
        aux acc next_off sizes
    in
    aux ([], 0) off sizes


  (* Contents in memory. The type of function definitions varies from a language
     to another; thus, it is left generic. *)

  type 'fun_def content =
    | Contents of contents
    | Fun_def of 'fun_def


  (* The mapping from blocks to contents. *)

  module BlockMap = Map.Make (Block)
  type 'fun_def blockMap = 'fun_def content BlockMap.t
  type block = Block.t

  (* The mapping from global identifiers to blocks (negative for function
     definitions and positive for global variables). *)

  module GlobalMap = Map.Make (String)
  type globalMap = Value.t GlobalMap.t

  (* The memory.
     It is a mapping from blocks to contents, a mapping from global identifiers
     (variables and functions) to pointers, a mapping from (negative) blocks to
     function definition, the next free positive block and the next free
     negative block. *)

  type 'fun_def memory =
      { blocks           : 'fun_def blockMap ;
        addr_of_global   : globalMap ;
        next_block       : block ;
        next_fun_block   : block }

  (* Pretty printing *)

  let print mem = 
    let print_cells off = function
      | Datum (size, v) when Value.eq v Value.undef -> 
        ()
      | Datum (size, v) -> 
        Printf.printf "\n  %s: [%d,%s]%!"
          (Offset.to_string off) size (Value.to_string v)
      | Cont -> Printf.printf "[Cont]%!" in
    let print_block b content =
      Printf.printf "\nBlock %s: %!" (Block.to_string b) ;
      match content with
        | Contents contents ->
          Printf.printf "(%s -> %s)%!"
            (Offset.to_string contents.low) (Offset.to_string contents.high) ;
          OffsetMap.iter print_cells contents.cells
        | Fun_def _ -> Printf.printf "function definition%!" ;
    in 
    BlockMap.iter print_block mem.blocks ;
    Printf.printf "\n%!"


  (* Memory manipulation *)

  let empty =
    { blocks = BlockMap.empty ;
      addr_of_global = GlobalMap.empty ;
      next_block = Block.of_int 1 ;
      next_fun_block = Block.of_int (-1) }

  (* Memory allocation *)

  (** [write_interval contents lo_off hi_off d] writes the cell [d] in the
      contents [contents] from the offset [lo_off] (inclusive) to the offset
      [hi_off] (exclusive). *)
  let rec write_interval contents lo_off hi_off d =
    if Offset.ge lo_off hi_off then contents
    else
      let contents = add_cells contents lo_off d in
      write_interval contents (Offset.succ lo_off) hi_off d

  (** [alloc2 mem lo hi] allocates in memory [mem] a new block whose readable
      and writable offsets are the interval [lo] (inclusive) [hi]
      (exclusive). *)
  let alloc2 mem lo hi =
    let b = mem.next_block in
    let contents = { low = lo ; high = hi ; cells = OffsetMap.empty } in
    let contents = write_interval contents lo hi (Datum (1, Value.undef)) in
    let blocks = BlockMap.add b (Contents contents) mem.blocks in
    let next_block = Block.succ mem.next_block in
    let mem' = { mem with blocks = blocks ; next_block = next_block } in
    (mem', Value.of_pointer (b, lo))

  (** [alloc mem size] allocates a block of [size] size (in bytes) in the memory
      [mem]. It returns the new memory and a pointer to the beginning of the
      allocated area. *)
  let alloc mem size =
    alloc2 mem Offset.zero (Offset.of_int size)


  let size_of_mq = function
    | MQ_int8unsigned | MQ_int8signed -> 1
    | MQ_int16unsigned | MQ_int16signed -> 2
    | MQ_int32 | MQ_float32 -> 4
    | MQ_float64 -> 8
    | MQ_pointer -> D.ptr_size
    | MQ_chunk -> D.ptr_size/2

  let cast_of_mq = function
    | MQ_int8unsigned -> Value.cast8unsigned
    | MQ_int8signed -> Value.cast8signed
    | MQ_int16unsigned -> Value.cast16unsigned
    | MQ_int16signed -> Value.cast16signed
    | MQ_int32 -> Value.cast32
    | MQ_float32 | MQ_float64 -> error "float not supported."
    | MQ_pointer | MQ_chunk -> (fun v -> v)

  (* The 'safe'-prefixed functions below raise an error when the argument is not
     of the expected form. *)

  let safe_to_pointer msg v =
    if Value.is_pointer v then Value.to_pointer v
    else error msg

  let safe_find msg find a map =
    try find a map
    with Not_found -> error msg

  let safe_find_block msg b mem = safe_find msg BlockMap.find b mem.blocks

  let safe_find_contents msg b mem = match safe_find_block msg b mem with
    | Contents contents -> contents
    | Fun_def _ -> error msg

  let safe_find_offset msg off contents =
    safe_find msg OffsetMap.find off contents.cells

  let memory_find msg mem b off =
    safe_find_offset msg off (safe_find_contents msg b mem)

  (** [all_are_in_list msg mem b first_off last_off dl] returns [true] iff all
      the datas found in the block [b] of memory [mem] and between offsets
      [first_off] (inclusive) and [last_off] (exclusive) are in the list
      [dl]. *)
  let all_are_in_list msg mem b first_off last_off dl =
    let d_eq d d' = match d, d' with
      | Datum (size, v), Datum (size', v') -> (size = size') && (Value.eq v v')
      | Cont, Cont -> true
      | _ -> false in
    let rec aux d = function
      | [] -> false
      | d' :: dl -> (d_eq d d') || (aux d dl) in
    let dl_mem d = aux d dl in
    match safe_find_block msg b mem with
      | Contents contents
          when (Offset.le contents.low first_off) &&
            (Offset.le last_off contents.high) ->
        let rec aux off =
          if Offset.ge off last_off then true
          else
            if OffsetMap.mem off contents.cells then
              let d = OffsetMap.find off contents.cells in
              (dl_mem d) && (aux (Offset.succ off))
            else false
        in
        aux first_off
      | _ -> false

  (** [all_are_undef msg mem b first_off last_off] returns [true] iff all the
      datas found in the block [b] of memory [mem] and between offsets
      [first_off] (inclusive) and [last_off] (exclusive) are the undef value. *)
  let all_are_undef msg mem b first_off last_off =
    all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef)]

  (** [all_are_undef msg mem b first_off last_off] returns [true] iff all the
      datas found in the block [b] of memory [mem] and between offsets
      [first_off] (inclusive) and [last_off] (exclusive) are the undef value or
      the Cont cell. *)
  let all_are_undef_or_cont msg mem b first_off last_off =
    all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef) ; Cont]

  let string_of_alignment = function
    | None -> "none"
    | Some alignment -> string_of_int alignment

  (** [write_value msg mem b off size v size'] store the value [v] at the offset
      [off] of the block [b] in the memory [mem]. [size] is the size of the
      value [v], and [size'] >= [size] is the number of bytes that are actually
      written. When [size'] > [size], the undefined value is used to fill the
      remaining memory cells. *)
  let write_value msg mem b off size v size' =
    if not (is_aligned off size) then
      error "Alignment constraint violated when storing value."
    else
      let shift_off n = Offset.add off (Offset.of_int n) in
      match safe_find_block msg b mem with
        | Contents contents
            when (Offset.le contents.low off) &&
              (Offset.le (shift_off size) contents.high) ->
          let contents = add_cells contents off (Datum (size, v)) in
          let contents =
            write_interval contents (Offset.succ off) (shift_off size) Cont in
          let contents =
            write_interval contents (shift_off size) (shift_off size')
              (Datum (1, Value.undef)) in
          let blocks = BlockMap.add b (Contents contents) mem.blocks in
          { mem with blocks = blocks }
        | _ -> error msg


  (* Memory free *)

  let free mem addr =
    if Value.is_pointer addr then
      let (b, _) = Value.to_pointer addr in
      { mem with blocks = BlockMap.remove b mem.blocks }
    else error "free: invalid memory address."


  (* Memory load and store *)

  (** [load2 mem size addr] reads a value of size [size] at the address [addr]
      in memory [mem]. *)
  let load2 mem size addr =
    let msg = ("load: invalid memory access. ("^(Value.to_string addr)^")") in
    let (b, off) = safe_to_pointer msg addr in
    if not (is_aligned off size) then
      error "Alignment constraint violated when loading value."
    else
      match memory_find msg mem b off with
        | Datum (size', v) when size <= size' -> 
          v
              (*print_string ("Db: load m "^(string_of_memory_q chunk)^" "
                            ^(Value.to_string addr)^" "^(Value.to_string r)^" ("
                            ^(Value.to_string v)^")\n"); *)
        | _ -> print mem;error msg

  (** [load mem chunk addr] reads a value of type [chunk] at the address [addr]
      in memory [mem]. *)
  let load mem chunk addr =
    let size = size_of_mq chunk in
    cast_of_mq chunk (load2 mem size addr)


  (** [write_undef_before msg mem b off] replaces with undefined values the
      value whose last cell is at offset [off] of block [b] in memory
      [mem]. *)
  let write_undef_before msg mem b off =
    let contents = safe_find_contents msg b mem in
    let d = Datum (1, Value.undef) in
    let rec aux off contents =
      if OffsetMap.mem off contents.cells then
        let contents' = add_cells contents off d in
        match OffsetMap.find off contents.cells with
          | Datum _ -> contents'
          | Cont -> aux (Offset.pred off) contents'
      else contents
    in
    let contents = aux off contents in
    { mem with blocks = BlockMap.add b (Contents contents) mem.blocks }

  (** [store2 mem size addr v] writes the value [v] of size [size] at address
      [addr] in memory [mem]. *)
  let store2 mem size addr v =
    let msg = "store: invalid memory access." in
    let (b, off) = safe_to_pointer msg addr in
    let shift_off n = Offset.add off (Offset.of_int n) in
    (*print_string ("Db: store m "^(string_of_memory_q chunk)^" "
      ^(Value.to_string addr)^" "^(Value.to_string v)^" ("
      ^(Value.to_string v0)^")\n"); *)
    match memory_find msg mem b off with
      | Datum (size', _) when size <= size' ->
          write_value msg mem b off size v size'
      | Datum (size', _)
          when all_are_undef msg mem b (shift_off size') (shift_off size) ->
          write_value msg mem b off size v size'
      | Cont when all_are_undef_or_cont msg mem b off (shift_off size) ->
          let mem = write_value msg mem b off size v size in 
          write_undef_before msg mem b (Offset.pred off)
      | _ -> error msg

  (** [store mem chunk addr v] writes the value [v] interpreted as a value of
      type [chunk] at address [addr] in memory [mem]. *)
  let store mem chunk addr v =
    store2 mem (size_of_mq chunk) addr (cast_of_mq chunk v)


(* Data manipulation *)

  let value_of_data = function
    | AST.Data_reserve _ -> Value.undef
    | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i -> Value.of_int i
    | AST.Data_float32 f | AST.Data_float64 f -> Value.of_float f

  let size_of_data = function
    | AST.Data_reserve n -> n
    | data -> size_of_mq (mq_of_data data)

  let offsets_size_of_datas datas =
    align Offset.zero (List.map size_of_data datas)

  (** [alloc_datas mem datas] returns the memory and the address obtained by
      allocating space and storing the datas [datas] in the memory [mem]. *)
  let alloc_datas mem datas =
    let (offs_of_datas, size) = offsets_size_of_datas datas in
    let (mem, addr) = alloc mem size in
    let shift_addr off = Value.add addr (Value.of_int_repr off) in
    let f mem data off = match data with
      | AST.Data_reserve _ -> mem
      | _ -> store mem (mq_of_data data) (shift_addr off) (value_of_data data)
    in
    (List.fold_left2 f mem datas offs_of_datas, addr)

  let size_of_datas datas = snd (offsets_size_of_datas datas)

  (** [offsets_of_datas datas] returns the aligned offsets for the datas
      [datas], starting at offset 0. *)
  let offsets_of_datas datas =
    let (offs_of_datas, _) = offsets_size_of_datas datas in
    List.combine datas (List.map Offset.to_int offs_of_datas)

  (** [align off sizes] returns the aligned offsets (starting at [off]) of datas
      of size [sizes]. *)
  let align off sizes =
    let (offsets, size) = align (Offset.of_int off) sizes in
    (List.map Offset.to_int offsets, size)


  (* Global environment manipulation *)

  (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of
      memory [mem], and associates the global variable [x] with the address of
      the block. *)
  let add_var mem v_id datas =
    let (mem, addr) = alloc_datas mem datas in
    let addr_of_global = GlobalMap.add v_id addr mem.addr_of_global in
    { mem with addr_of_global = addr_of_global }

  (** [add_fun_def mem f def] stores the function definition [def] in a new
      block of memory [mem], and associates the function name [f] with the
      address of the block. *)
  let add_fun_def mem f_id f_def =
    let b = mem.next_fun_block in
    let next_fun_block = Block.pred mem.next_fun_block in
    let addr = Value.of_pointer (b, Offset.zero) in
    let addr_of_global = GlobalMap.add f_id addr mem.addr_of_global in
    let blocks = BlockMap.add b (Fun_def f_def) mem.blocks in
    { mem with blocks = blocks ;
               addr_of_global = addr_of_global ;
               next_fun_block = next_fun_block }

  (** [find_global mem x] returns the address associated with the global symbol
      [x] in memory [mem]. [x] may be a global variable or the name of a
      function. *)
  let find_global mem gid =
    if GlobalMap.mem gid mem.addr_of_global then
      GlobalMap.find gid mem.addr_of_global
    else error ("Unknown global \"" ^ gid ^ "\"")

  (** [find_fun_def mem addr] returns the function definition found at address
      [addr] in memory [mem]. Raises an error if no function definition is
      found. *)
  let find_fun_def mem v =
    let msg = "Invalid access to a function definition." in
    let (b, _) = safe_to_pointer msg v in
    match safe_find_block msg b mem with
      | Contents _ -> error msg
      | Fun_def def -> def


  

end