src/languages.mli

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