source: Deliverables/D2.2/8051-indexed-labels-branch/src/languages.mli @ 1433

Last change on this file since 1433 was 1433, checked in by tranquil, 9 years ago
  • added infrastructure to add same-language transformations along the compilation chain from command line options
  • started work on cost expression semplification
File size: 3.4 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
33(** The type of additional transfromations, with the language they take place
34    in and the actual transformation *)
35type transformation = name * (ast -> ast)
36
37(** [language_of_ast ast] returns the programming language of the
38    abstract syntax tree [ast]. *)
39val language_of_ast : ast -> name
40
41(** [parse name] returns the parsing function of the language
42    [name]. *)
43val parse : name -> (string -> ast) 
44
45(** {2 Compilation} *)
46
47(** [compile debug ts l1 l2] returns the compilation function that
48    translates the language [l1] to the language [l2], employing the
49                transformations in [ts] along the way . This may be the
50    composition of several compilation functions. If [debug] is
51    [true], all the intermediate programs are inserted in the
52    output. *)
53val compile : bool -> transformation list -> name -> name -> (ast -> ast list)
54
55(** [add_runtime ast] adds runtime functions for the operations not supported by
56    the target processor. *)
57val add_runtime : ast -> ast
58
59(** {2 Annotation}
60
61    Labelling consists in the insertion of so-called "cost labels"
62    which are useful control points in order to compute costs.
63
64    The annotation process first computes cost of constant-time
65    execution path starting from each cost label on the lowest-level
66    language. Then, it instruments the (high-level) source code with
67    these computed costs.
68*)
69
70(** [labelize ast] inserts cost labels in the program [ast]. *)
71val labelize : ast -> ast
72
73(** [annotate input_ast target_ast] inserts cost annotations into the input AST
74    from the (final) target AST. It also returns the name of the cost variable
75    and the name of the cost increment function. *)
76val annotate : ast -> ast -> (ast * string * string)
77
78(** [interpret debug ast] runs the program [ast] from the default initial
79    configuration. This interpretation may emit some cost labels. *)
80val interpret : bool -> ast -> AST.trace
81
82(** {2 Serialization} *)
83
84(** [save exact_output filename input_ast] pretty prints [input_ast] in a file
85    whose name is prefixed by [filename] and whose extension is deduced from the
86    language of the AST. If [exact_output] is false then the written file will
87    be fresh. *)
88val save : bool -> string -> string -> ast -> unit
89
90(** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
91    cost variable and then the name [cost_incr] of the cost increment function
92    in a seperate line in the file prefixed by [filename] and extended with
93    ".cost". If the file already exists, it is overwritten. *)
94val save_cost : string -> string -> string -> unit
95
96(** [from_string s] parses [s] as an intermediate language name. *)
97val from_string : string -> name
98
99(** [to_string n] prints [n] as a string. *)
100val to_string   : name -> string
Note: See TracBrowser for help on using the repository browser.