]> matita.cs.unibo.it Git - pkg-cerco/acc.git/blob - src/common/memory.mli
Package description and copyright added.
[pkg-cerco/acc.git] / 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