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

Last change on this file since 1507 was 1507, checked in by tranquil, 9 years ago
  • added an option to not use ternary expressions in costs, to accomodate frama-c explosion of such expressions
  • corrected some typos in comments
  • added a check for well behaved for loops in loop unrolling, but intelligent unrolling is not done yet
  • TODO: peeling and unrolling can contradict preciseness (with difference between introduced branches around 2 cycles). I guess it can be corrected easily
File size: 3.5 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 cost_tern input_ast target_ast] inserts cost annotations into the
74    input AST from the (final) target AST. It also returns the name of the cost
75    variable and the name of the cost increment function. The [cost_tern] flag
76    rules whether cost increments are given by ternary expressions or branch
77    statements. *)
78val annotate : bool -> ast -> ast -> (ast * string * string)
79
80(** [interpret debug ast] runs the program [ast] from the default initial
81    configuration. This interpretation may emit some cost labels. *)
82val interpret : bool -> ast -> AST.trace
83
84(** {2 Serialization} *)
85
86(** [save exact_output filename input_ast] pretty prints [input_ast] in a file
87    whose name is prefixed by [filename] and whose extension is deduced from the
88    language of the AST. If [exact_output] is false then the written file will
89    be fresh. *)
90val save : bool -> string -> string -> ast -> unit
91
92(** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
93    cost variable and then the name [cost_incr] of the cost increment function
94    in a seperate line in the file prefixed by [filename] and extended with
95    ".cost". If the file already exists, it is overwritten. *)
96val save_cost : string -> string -> string -> unit
97
98(** [from_string s] parses [s] as an intermediate language name. *)
99val from_string : string -> name
100
101(** [to_string n] prints [n] as a string. *)
102val to_string   : name -> string
Note: See TracBrowser for help on using the repository browser.