src/common/memory.mli

   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 val string_of_quantity : AST.quantity -> string
  10
  11 val size_of_data  : AST.data -> int
  12
  13 val all_offsets : AST.abstract_size -> AST.abstract_offset list list
  14
  15
  16 (** This is the signature of the parameter module of the functor. *)
  17
  18 module type DATA_SIZE =
  19 sig
  20   val int_size  : int
  21   val ptr_size  : int
  22   val alignment : int option
  23 end
  24
  25
  26 (** This is the signature of the module that provides functions and types to
  27     manipulate memories. *)
  28
  29 module type S =
  30 sig
  31
  32   val int_size  : int
  33   val ptr_size  : int
  34   val alignment : int option
  35
  36   val size_of_quantity : AST.quantity -> int
  37
  38   module Value : Value.S
  39
  40   (* Memory. A memory contains values and function definitions. Since the memory
  41      module will be used by the interpreters of the various languages of the
  42      compilation chain, the type of memory is polymorphic with the type of
  43      function definitions. *)
  44
  45   type 'fun_def memory
  46
  47   (* Memory manipulation *)
  48
  49   val empty : 'fun_def memory
  50
  51   (** [alloc mem size] allocates a block of [size] bytes in the memory [mem]. It
  52       returns the new memory and the address of the beginning of the newly
  53       allocated area. *)
  54   val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.address
  55
  56   (* Memory free *)
  57
  58   val free : 'fun_def memory -> Value.address -> 'fun_def memory
  59
  60   (* Memory load and store *)
  61
  62   (** [load mem size addr] reads [size] bytes from address [addr] in memory
  63       [mem] and returns the value found. *)
  64   val load  : 'fun_def memory -> int -> Value.address -> Value.t
  65   val loadq : 'fun_def memory -> AST.quantity -> Value.address -> Value.t
  66
  67   (** [store mem size addr v] writes the [size] first bytes (little endian
  68       representation) of value [v] at address [addr] in memory [mem]. *)
  69   val store  : 'fun_def memory -> int -> Value.address -> Value.t ->
  70                'fun_def memory
  71   val storeq : 'fun_def memory -> AST.quantity -> Value.address -> Value.t ->
  72                'fun_def memory
  73
  74   (* Globals management *)
  75
  76   (** [add_var mem x offsets init_datas] stores the datas [init_datas] of
  77       offsets [offsets] in a new block of memory [mem], and associates the
  78       global variable [x] with the address of the block. *)
  79   val add_var :
  80     'fun_def memory -> AST.ident -> AST.abstract_size -> AST.data list option ->
  81     'fun_def memory
  82
  83   (** [add_fun_def mem f def] stores the function definition [def] in a new
  84       block of memory [mem], and associates the function name [f] with the
  85       address of the block. *)
  86   val add_fun_def : 'fun_def memory -> AST.ident -> 'fun_def -> 'fun_def memory
  87
  88   val mem_global : 'fun_def memory -> AST.ident -> bool
  89
  90   (** [find_global mem x] returns the address associated with the global symbol
  91       [x] in memory [mem]. [x] may be a global variable or the name of a
  92       function. *)
  93   val find_global : 'fun_def memory -> AST.ident -> Value.address
  94
  95   (** [find_fun_def mem addr] returns the function definition found at address
  96       [addr] in memory [mem]. Raises an error if no function definition is
  97       found. *)
  98   val find_fun_def : 'fun_def memory -> Value.address -> 'fun_def
  99
 100
 101   (** [align off size] returns the aligned offsets (starting at [off]) of datas
 102       of size [size]. *)
 103   val align : int (* starting offset *) -> AST.abstract_size (* sizes *) ->
 104               (int list (* resulting offsets *) * int (* full size *))
 105
 106   val concrete_offsets_size : AST.abstract_size -> int list * int
 107
 108   val concrete_offsets : AST.abstract_size -> int list
 109
 110   val concrete_size : AST.abstract_size -> int
 111
 112   val concrete_offset : AST.abstract_offset -> int
 113
 114 (*
 115   val size_of_datas : AST.data list -> int
 116
 117   (** [offsets_of_datas datas] returns the aligned offsets for the datas
 118       [datas], starting at offset 0. *)
 119   val offsets_of_datas : AST.data list -> (AST.data * int (* offset *)) list
 120
 121   val alloc_datas : 'fun_def memory -> AST.data list ->
 122                     ('fun_def memory * Value.address)
 123 *)
 124
 125   val to_string : 'fun_def memory -> string
 126   val print : 'fun_def memory -> unit
 127
 128 end
 129
 130
 131 (** The functor to a memory module. *)
 132
 133 module Make (D : DATA_SIZE) : S