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 are expressed in bytes. *) |
---|
7 | |
---|
8 | |
---|
9 | (* Memory quantities are the size and the type of what can be loaded |
---|
10 | and stored in memory *) |
---|
11 | |
---|
12 | type memory_q = |
---|
13 | | MQ_int8signed | MQ_int8unsigned | MQ_int16signed | MQ_int16unsigned |
---|
14 | | MQ_int32 | MQ_float32 | MQ_float64 | MQ_pointer |
---|
15 | | MQ_chunk (* no type, just the raw content of a word size *) |
---|
16 | |
---|
17 | val string_of_memory_q : memory_q -> string |
---|
18 | |
---|
19 | val mq_of_data : AST.data -> memory_q |
---|
20 | |
---|
21 | val type_of_memory_q : memory_q -> AST.sig_type |
---|
22 | |
---|
23 | |
---|
24 | (** This is the signature of the parameter module of the functor. *) |
---|
25 | |
---|
26 | module type DATA_SIZE = |
---|
27 | sig |
---|
28 | val int_size : int (* in bytes *) |
---|
29 | val ptr_size : int (* in bytes *) |
---|
30 | val alignment : int option (* in bytes, if any *) |
---|
31 | end |
---|
32 | |
---|
33 | |
---|
34 | (** This is the signature of the module that provides functions and types to |
---|
35 | manipulate memories. *) |
---|
36 | |
---|
37 | module type S = |
---|
38 | sig |
---|
39 | |
---|
40 | val mq_of_ptr : memory_q |
---|
41 | val int_size : int |
---|
42 | val ptr_size : int |
---|
43 | val alignment : int option |
---|
44 | |
---|
45 | module Value : Value.S |
---|
46 | |
---|
47 | (* Memory. A memory contains values and function definitions. Since the memory |
---|
48 | module will be used by the interpreters of the various languages of the |
---|
49 | compilation chain, the type of memory is polymorphic with the type of |
---|
50 | function definitions. *) |
---|
51 | |
---|
52 | type 'fun_def memory |
---|
53 | |
---|
54 | (* Memory manipulation *) |
---|
55 | |
---|
56 | val empty : 'fun_def memory |
---|
57 | |
---|
58 | (** [alloc mem size] allocates a block of [size] size (in bytes) in the memory |
---|
59 | [mem]. It returns the new memory and a pointer to the beginning of the |
---|
60 | allocated area. *) |
---|
61 | val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.t |
---|
62 | |
---|
63 | (* Memory free *) |
---|
64 | |
---|
65 | val free : 'fun_def memory -> Value.t -> 'fun_def memory |
---|
66 | |
---|
67 | (* Memory load and store *) |
---|
68 | |
---|
69 | (** [load mem chunk addr] reads a value of type [chunk] at the address [addr] |
---|
70 | in memory [mem]. *) |
---|
71 | val load : 'fun_def memory -> memory_q -> Value.t -> Value.t |
---|
72 | (** [load2 mem size addr] reads a value of size [size] at the address [addr] |
---|
73 | in memory [mem]. *) |
---|
74 | val load2 : 'fun_def memory -> int -> Value.t -> Value.t |
---|
75 | |
---|
76 | (** [store mem chunk addr v] writes the value [v] interpreted as a value of |
---|
77 | type [chunk] at address [addr] in memory [mem]. *) |
---|
78 | val store : 'fun_def memory -> memory_q -> Value.t -> Value.t -> |
---|
79 | 'fun_def memory |
---|
80 | (** [store2 mem size addr v] writes the value [v] of size [size] at address |
---|
81 | [addr] in memory [mem]. *) |
---|
82 | val store2 : 'fun_def memory -> int -> Value.t -> Value.t -> |
---|
83 | 'fun_def memory |
---|
84 | |
---|
85 | (** [add_var mem x init_datas] stores the datas [init_datas] in a new block of |
---|
86 | memory [mem], and associates the global variable [x] with the address of |
---|
87 | the block. *) |
---|
88 | val add_var : 'fun_def memory -> AST.ident -> AST.data list -> 'fun_def memory |
---|
89 | |
---|
90 | (** [add_fun_def mem f def] stores the function definition [def] in a new |
---|
91 | block of memory [mem], and associates the function name [f] with the |
---|
92 | address of the block. *) |
---|
93 | val add_fun_def : 'fun_def memory -> AST.ident -> 'fun_def -> 'fun_def memory |
---|
94 | |
---|
95 | (** [find_global mem x] returns the address associated with the global symbol |
---|
96 | [x] in memory [mem]. [x] may be a global variable or the name of a |
---|
97 | function. *) |
---|
98 | val find_global : 'fun_def memory -> AST.ident -> Value.t |
---|
99 | |
---|
100 | (** [find_fun_def mem addr] returns the function definition found at address |
---|
101 | [addr] in memory [mem]. Raises an error if no function definition is |
---|
102 | found. *) |
---|
103 | val find_fun_def : 'fun_def memory -> Value.t -> 'fun_def |
---|
104 | |
---|
105 | (** [align off sizes] returns the aligned offsets (starting at [off]) of datas |
---|
106 | of size [sizes]. *) |
---|
107 | val align : int (* starting offset *) -> int list (* sizes *) -> |
---|
108 | (int list (* resulting offsets *) * int (* full size *)) |
---|
109 | |
---|
110 | val size_of_datas : AST.data list -> int |
---|
111 | |
---|
112 | (** [offsets_of_datas datas] returns the aligned offsets for the datas |
---|
113 | [datas], starting at offset 0. *) |
---|
114 | val offsets_of_datas : AST.data list -> (AST.data * int (* offset *)) list |
---|
115 | |
---|
116 | val alloc_datas : 'fun_def memory -> AST.data list -> |
---|
117 | ('fun_def memory * Value.t) |
---|
118 | |
---|
119 | val print : 'fun_def memory -> unit |
---|
120 | |
---|
121 | end |
---|
122 | |
---|
123 | |
---|
124 | (** The functor to a memory module. *) |
---|
125 | |
---|
126 | module Make (D : DATA_SIZE) : S |
---|