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

(** This module defines the intermediate languages. 

    This is a dispatching module that is aware of the whole
    compilation chain. It can also be used as an homogeneous way to
    deal with the intermediate languages functionalities.
*)


type name = 
  | Clight
  | Cminor
  | RTLabs
  | RTL
  | ERTL
  | LTL
  | LIN
  | ASM

(** {2 Abstract syntax trees} *)

(** The types of abstract syntax trees of each language. *)
type ast = 
  | AstClight of Clight.program
  | AstCminor of Cminor.program
  | AstRTLabs of RTLabs.program
  | AstRTL    of RTL.program
  | AstERTL   of ERTL.program
  | AstLTL    of LTL.program
  | AstLIN    of LIN.program
  | AstASM    of ASM.program

(** [language_of_ast ast] returns the programming language of the 
    abstract syntax tree [ast]. *)
val language_of_ast : ast -> name

(** [parse name] returns the parsing function of the language
    [name]. *)
val parse : name -> (string -> ast) 

(** {2 Compilation} *)

(** [compile debug l1 l2] returns the compilation function that
    translates the language [l1] to the language [l2]. This may be the
    composition of several compilation functions. If [debug] is
    [true], all the intermediate programs are inserted in the
    output. *)
val compile : bool -> name -> name -> (ast -> ast list)

(** {2 Annotation} 

    Labelling consists in the insertion of so-called "cost labels" 
    which are useful control points in order to compute costs.

    The annotation process first computes cost of constant-time
    execution path starting from each cost label on the lowest-level
    language. Then, it instruments the (high-level) source code with
    these computed costs.
*)

(** [labelize ast] inserts cost labels in the program [ast]. *)
val labelize : ast -> ast

(** [annotate input_ast target_ast] inserts cost annotations into the input AST
    from the (final) target AST. It also returns the name of the cost variable
    and the name of the cost increment function. *)
val annotate : ast -> ast -> (ast * string * string)

(** [interpret debug ast] runs the program [ast] from the default initial
    configuration. This interpretation may emit some cost labels. *)
val interpret : bool -> ast -> AST.trace

(** {2 Serialization} *)

(** [save exact_output filename input_ast] pretty prints [input_ast] in a file
    whose name is prefixed by [filename] and whose extension is deduced from the
    language of the AST. If [exact_output] is false then the written file will
    be fresh. *)
val save : bool -> string -> string -> ast -> unit

(** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
    cost variable and then the name [cost_incr] of the cost increment function
    in a seperate line in the file prefixed by [filename] and extended with
    ".cost". If the file already exists, it is overwritten. *)
val save_cost : string -> string -> string -> unit

(** [from_string s] parses [s] as an intermediate language name. *)
val from_string : string -> name

(** [to_string n] prints [n] as a string. *)
val to_string   : name -> string