source: Deliverables/D2.2/8051/src/languages.mli @ 818

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

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

File size: 3.2 KB
Line 
1(** This module defines the intermediate languages.
2
3    This is a dispatching module that is aware of the whole
4    compilation chain. It can also be used as an homogeneous way to
5    deal with the intermediate languages functionalities.
6*)
7
8
9type name = 
10  | Clight
11  | Cminor
12  | RTLabs
13  | RTL
14  | ERTL
15  | LTL
16  | LIN
17  | ASM
18
19(** {2 Abstract syntax trees} *)
20
21(** The types of abstract syntax trees of each language. *)
22type ast = 
23  | AstClight  of Clight.program
24  | AstCminor  of Cminor.program
25  | AstRTLabs  of RTLabs.program
26  | AstRTL     of RTL.program
27  | AstERTL    of ERTL.program
28  | AstLTL     of LTL.program
29  | AstLIN     of LIN.program
30  | AstASM     of ASM.program
31
32(** [language_of_ast ast] returns the programming language of the
33    abstract syntax tree [ast]. *)
34val language_of_ast : ast -> name
35
36(** [parse name] returns the parsing function of the language
37    [name]. *)
38val parse : name -> (string -> ast) 
39
40(** {2 Compilation} *)
41
42(** [compile debug l1 l2] returns the compilation function that
43    translates the language [l1] to the language [l2]. This may be the
44    composition of several compilation functions. If [debug] is
45    [true], all the intermediate programs are inserted in the
46    output. *)
47val compile : bool -> name -> name -> (ast -> ast list)
48
49(** [add_runtime ast] adds runtime functions for the operations not supported by
50    the target processor. *)
51val add_runtime : ast -> ast
52
53(** {2 Annotation}
54
55    Labelling consists in the insertion of so-called "cost labels"
56    which are useful control points in order to compute costs.
57
58    The annotation process first computes cost of constant-time
59    execution path starting from each cost label on the lowest-level
60    language. Then, it instruments the (high-level) source code with
61    these computed costs.
62*)
63
64(** [labelize ast] inserts cost labels in the program [ast]. *)
65val labelize : ast -> ast
66
67(** [annotate input_ast target_ast] inserts cost annotations into the input AST
68    from the (final) target AST. It also returns the name of the cost variable
69    and the name of the cost increment function. *)
70val annotate : ast -> ast -> (ast * string * string)
71
72(** [interpret debug ast] runs the program [ast] from the default initial
73    configuration. This interpretation may emit some cost labels. *)
74val interpret : bool -> ast -> AST.trace
75
76(** {2 Serialization} *)
77
78(** [save exact_output filename input_ast] pretty prints [input_ast] in a file
79    whose name is prefixed by [filename] and whose extension is deduced from the
80    language of the AST. If [exact_output] is false then the written file will
81    be fresh. *)
82val save : bool -> string -> string -> ast -> unit
83
84(** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
85    cost variable and then the name [cost_incr] of the cost increment function
86    in a seperate line in the file prefixed by [filename] and extended with
87    ".cost". If the file already exists, it is overwritten. *)
88val save_cost : string -> string -> string -> unit
89
90(** [from_string s] parses [s] as an intermediate language name. *)
91val from_string : string -> name
92
93(** [to_string n] prints [n] as a string. *)
94val to_string   : name -> string
Note: See TracBrowser for help on using the repository browser.