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

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

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 3.0 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 debug ast] runs the program [ast] from the default initial
69    configuration. This interpretation may emit some cost labels. *)
70val interpret : bool -> ast -> AST.trace
71
72(** {2 Serialization} *)
73
74(** [save exact_output filename input_ast] pretty prints [input_ast] in a file
75    whose name is prefixed by [filename] and whose extension is deduced from the
76    language of the AST. If [exact_output] is false then the written file will
77    be fresh. *)
78val save : bool -> string -> string -> ast -> unit
79
80(** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
81    cost variable and then the name [cost_incr] of the cost increment function
82    in a seperate line in the file prefixed by [filename] and extended with
83    ".cost". If the file already exists, it is overwritten. *)
84val save_cost : string -> string -> string -> unit
85
86(** [from_string s] parses [s] as an intermediate language name. *)
87val from_string : string -> name
88
89(** [to_string n] prints [n] as a string. *)
90val to_string   : name -> string
Note: See TracBrowser for help on using the repository browser.