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
RevLine 
[486]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 = 
[818]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
[486]31
[1433]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
[486]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
[1433]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
[486]50    composition of several compilation functions. If [debug] is
51    [true], all the intermediate programs are inserted in the
52    output. *)
[1433]53val compile : bool -> transformation list -> name -> name -> (ast -> ast list)
[486]54
[818]55(** [add_runtime ast] adds runtime functions for the operations not supported by
56    the target processor. *)
57val add_runtime : ast -> ast
58
[486]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
[619]73(** [annotate input_ast target_ast] inserts cost annotations into the input AST
[640]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)
[486]77
[740]78(** [interpret debug ast] runs the program [ast] from the default initial
79    configuration. This interpretation may emit some cost labels. *)
[619]80val interpret : bool -> ast -> AST.trace
[486]81
82(** {2 Serialization} *)
83
[619]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. *)
[740]88val save : bool -> string -> string -> ast -> unit
[486]89
[640]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
[619]93    ".cost". If the file already exists, it is overwritten. *)
[640]94val save_cost : string -> string -> string -> unit
[619]95
[486]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.