source: Deliverables/D2.2/8051/src/common/memory.mli @ 619

(** 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. *)

(** In the module, every size are expressed in bytes. *)


(* 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 (* no type, just the raw content of a word size *)

val string_of_memory_q : memory_q -> string

val mq_of_data : AST.data -> memory_q

val type_of_memory_q : memory_q -> AST.sig_type


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

module type DATA_SIZE =
sig
  val int_size  : int (* in bytes *)
  val ptr_size  : int (* in bytes *)
  val alignment : int option (* in bytes, if any *)
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
  (** [store2 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) : S