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

Last change on this file since 1462 was 1462, checked in by ayache, 8 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

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