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

Last change on this file since 1664 was 1542, checked in by tranquil, 8 years ago

merge of indexed labels branch

File size: 4.7 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 ?is_lustre_file ?remove_lustre_externals name] returns the parsing
42    function of the language [name]. *)
43val parse : ?is_lustre_file:bool -> ?remove_lustre_externals:bool ->
44  name -> (string -> ast) 
45
46(** {2 Compilation} *)
47
48(** [compile debug ts l1 l2] returns the compilation function that
49    translates the language [l1] to the language [l2], employing the
50    transformations in [ts] along the way . This may be the
51    composition of several compilation functions. If [debug] is
52    [true], all the intermediate programs are inserted in the
53    output. *)
54val compile : bool -> transformation list -> name -> name -> (ast -> ast list)
55
56(** [add_runtime ast] adds runtime functions for the operations not supported by
57    the target processor. *)
58val add_runtime : ast -> ast
59
60(** {2 Annotation}
61
62    Labelling consists in the insertion of so-called "cost labels"
63    which are useful control points in order to compute costs.
64
65    The annotation process first computes cost of constant-time
66    execution path starting from each cost label on the lowest-level
67    language. Then, it instruments the (high-level) source code with
68    these computed costs.
69*)
70
71(** [labelize ast] inserts cost labels in the program [ast]. *)
72val labelize : ast -> ast
73
74(** [annotate cost_tern input_ast target_ast] inserts cost annotations into the
75    input AST from the (final) target AST. It also returns the name of the cost
76    variable and the name of the cost increment function, and a the name of a fresh
77    uninitialized global variable for each external function. The [cost_tern] flag
78    rules whether cost increments are given by ternary expressions or branch
79    statements. *)
80val annotate : bool -> ast -> ast -> (ast * string * string * string StringTools.Map.t)
81
82(** [interpret debug ast] runs the program [ast] from the default initial
83    configuration. This interpretation may emit some cost labels. *)
84val interpret : bool -> ast -> AST.trace
85
86(** {2 Serialization} *)
87
88(** [save asm_pretty exact_output filename suffix input_ast] prints [input_ast]
89    in a file whose name is prefixed by [filename], suffixed by [suffix] and
90    whose extension is deduced from the language of the AST. If [exact_output]
91    is false then the written file will be fresh. If [asm_pretty] is true, then
92    an additional pretty-printed assembly file is output. *)
93val save : bool -> bool -> string -> string -> ast -> unit
94
95(** [save_cost exact_name filename cost_id cost_incr extern_cost_variables]
96    prints the name [cost_id] of the cost variable, then the name [cost_incr] of
97    the cost increment function, and the entries of the mapping
98    [extern_cost_variables] (key first, then binding, seperated by a space) in a
99    seperate line in the file prefixed by [filename] and extended with
100    ".cost". If the file already exists, it is overwritten. *)
101val save_cost : bool -> string -> string -> string ->
102  string StringTools.Map.t -> unit
103
104(** [from_string s] parses [s] as an intermediate language name. *)
105val from_string : string -> name
106
107(** [to_string n] prints [n] as a string. *)
108val to_string   : name -> string
109
110(** [add_lustre_main lustre_test lustre_test_cases lustre_test_cycles
111    lustre_test_min_int lustre_test_max_int ast] adds a main function that tests
112    a Lustre step function to a Clight AST. The file [lustre_test] contains
113    CerCo information (e.g. the name of the cost variable). The integer
114    [lustre_test_cases] is the number of test cases that are performed, and the
115    integer [lustre_test_cycles] is the number of cycles per test
116    case. [lustre_test_min_int] (resp. [lustre_test_max_int]) is the minimum
117    (resp. maximum) integer value randomly generated during testing, and. *)
118val add_lustre_main : string -> int -> int -> int -> int -> ast -> ast
Note: See TracBrowser for help on using the repository browser.