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

Last change on this file since 640 was 640, checked in by ayache, 10 years ago

Hex output not too long for mcu anymore. Readable output added.

File size: 3.1 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(** {2 Annotation}
50
51    Labelling consists in the insertion of so-called "cost labels"
52    which are useful control points in order to compute costs.
53
54    The annotation process first computes cost of constant-time
55    execution path starting from each cost label on the lowest-level
56    language. Then, it instruments the (high-level) source code with
57    these computed costs.
58*)
59
60(** [labelize ast] inserts cost labels in the program [ast]. *)
61val labelize : ast -> ast
62
63(** [annotate input_ast target_ast] inserts cost annotations into the input AST
64    from the (final) target AST. It also returns the name of the cost variable
65    and the name of the cost increment function. *)
66val annotate : ast -> ast -> (ast * string * string)
67
68(** [interpret print_result ast] runs the program [ast] from the default initial
69    configuration. This interpretation may emit some cost labels. If
70    [print_result] is [true], then the result of the interpretations is
71    output. *)
72val interpret : bool -> ast -> AST.trace
73
74(** {2 Serialization} *)
75
76(** [save exact_output filename input_ast] pretty prints [input_ast] in a file
77    whose name is prefixed by [filename] and whose extension is deduced from the
78    language of the AST. If [exact_output] is false then the written file will
79    be fresh. *)
80val save : bool -> string -> ast -> unit
81
82(** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
83    cost variable and then the name [cost_incr] of the cost increment function
84    in a seperate line in the file prefixed by [filename] and extended with
85    ".cost". If the file already exists, it is overwritten. *)
86val save_cost : string -> string -> string -> unit
87
88(** [from_string s] parses [s] as an intermediate language name. *)
89val from_string : string -> name
90
91(** [to_string n] prints [n] as a string. *)
92val to_string   : name -> string
Note: See TracBrowser for help on using the repository browser.