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

Last change on this file since 1491 was 818, checked in by ayache, 9 years ago

32 and 16 bits operations support in D2.2/8051

File size: 4.2 KB
Line 
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
9val string_of_quantity : AST.quantity -> string
10
11val size_of_data  : AST.data -> int
12
13val 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
18module type DATA_SIZE =
19sig
20  val int_size  : int
21  val ptr_size  : int
22  val alignment : int option
23end
24
25
26(** This is the signature of the module that provides functions and types to
27    manipulate memories. *)
28
29module type S =
30sig
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
128end
129
130
131(** The functor to a memory module. *)
132
133module Make (D : DATA_SIZE) : S
Note: See TracBrowser for help on using the repository browser.