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

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

Deliverable D2.2

File size: 4.3 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 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
12type 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
17val string_of_memory_q : memory_q -> string
18
19val mq_of_data : AST.data -> memory_q
20
21val type_of_memory_q : memory_q -> AST.sig_type
22
23
24(** This is the signature of the parameter module of the functor. *)
25
26module type DATA_SIZE =
27sig
28  val int_size  : int (* in bytes *)
29  val ptr_size  : int (* in bytes *)
30  val alignment : int option (* in bytes, if any *)
31end
32
33
34(** This is the signature of the module that provides functions and types to
35    manipulate memories. *)
36
37module type S =
38sig
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
121end
122
123
124(** The functor to a memory module. *)
125
126module Make (D : DATA_SIZE) : S
Note: See TracBrowser for help on using the repository browser.