source: Deliverables/D2.3/8051/src/common/memory.mli @ 453

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

Import of the Paris's sources.

File size: 2.6 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
7(* Memory quantities are the size and the type of what can be loaded
8   and stored in memory *)
9
10type memory_q =
11  | MQ_int8signed | MQ_int8unsigned | MQ_int16signed | MQ_int16unsigned
12  | MQ_int32 | MQ_float32 | MQ_float64 | MQ_pointer | MQ_chunk
13
14val string_of_memory_q : memory_q -> string
15
16val mq_of_data : AST.data -> memory_q
17
18val type_of_memory_q : memory_q -> AST.sig_type
19
20
21module type DATA_SIZE =
22sig
23  val int_size  : int
24  val ptr_size  : int
25  val alignment : int option
26end
27
28
29module type S =
30sig
31
32  val mq_of_ptr : memory_q
33  val int_size  : int
34  val ptr_size  : int
35  val alignment : int option
36
37  module Value : Value.S
38
39  (* Memory *)
40
41  type 'fun_def memory
42
43  (* Memory manipulation *)
44
45  val empty : 'fun_def memory
46
47  (* Arguments are memory and size. *)
48  val alloc : 'fun_def memory -> int -> 'fun_def memory * Value.t
49
50  (* Memory free *)
51
52  val free : 'fun_def memory -> Value.t -> 'fun_def memory
53
54  (* Memory load and store *)
55
56  (* Arguments are memory, memory quantity, pointer value.
57     A cast is performed on the value to load. *)
58  val load : 'fun_def memory -> memory_q -> Value.t -> Value.t
59  (* Arguments are memory, size to load, pointer value. *)
60  val load2 : 'fun_def memory -> int -> Value.t -> Value.t
61
62  (* Arguments are memory, memory quantity, pointer value, new value. *)
63  val store  : 'fun_def memory -> memory_q -> Value.t -> Value.t ->
64               'fun_def memory
65  (* Arguments are memory, size to store, pointer value, new value.
66     A cast is performed on the value to store. *)
67  val store2 : 'fun_def memory -> int -> Value.t -> Value.t ->
68               'fun_def memory
69
70  val add_var : 'fun_def memory -> AST.ident -> AST.data list -> 'fun_def memory
71
72  val add_fun_def : 'fun_def memory -> AST.ident -> 'fun_def -> 'fun_def memory
73
74  val find_global : 'fun_def memory -> AST.ident -> Value.t
75
76  val find_fun_def : 'fun_def memory -> Value.t -> 'fun_def
77
78  (* Extra padding may be added at the end to satisfy alignment constraints. *)
79  val align : int (* starting offset *) -> int list (* sizes *) ->
80              (int list (* offsets *) * int (* full size *))
81
82  val size_of_datas    : AST.data list -> int
83  val offsets_of_datas : AST.data list -> (AST.data * int (* offset *)) list
84  val alloc_datas      : 'fun_def memory -> AST.data list ->
85                         ('fun_def memory * Value.t)
86
87  val print : 'fun_def memory -> unit
88
89end
90
91
92module Make (D : DATA_SIZE) : S
Note: See TracBrowser for help on using the repository browser.