Project

General

Profile

« Previous | Next » 

Revision 589ccf9f

Added by Corentin Lauverjat over 1 year ago

Passage à dune

View differences:

Dockerfile
1
FROM alpine:3.12 
2
# AS builder
3

  
4
RUN apk add --no-cache make m4 patch git pkgconfig libc-dev gcc \ 
5
    ocaml ocaml-compiler-libs ocaml-ocamldoc opam ocaml-findlib mpfr-dev \ 
6
    gmp-dev autoconf
7

  
8
# Configuration de OPAM
9
RUN opam init --auto-setup -y --disable-sandboxing && \
10
    eval $(opam config env)
11

  
12
# Installation de Z3 avec les bindings OCaml
13
RUN apk add perl python2 g++ &&  \
14
    opam install -y z3 && \
15
    opam clean
16

  
17
# Installation des autres dépendences projet
18
RUN opam install -y ocamlbuild depext ocamlgraph mlmpfr num cmdliner \
19
    fmt logs yojson menhir && \
20
    opam clean
21

  
22
# Copie des sources
23
COPY . /var/lustrec
24

  
25
WORKDIR /var/lustrec 
26

  
27
# Build
28
RUN eval $(opam env) && \
29
    autoconf && \
30
    ./configure && \
31
    make lustrec lustret && \
32
    mkdir -p /usr/local/include/lustrec && \
33
    ln include/*.h /usr/local/include/lustrec
34

  
35

  
36
#FROM alpine:3.12 
37
#
38
## GMP linking is dynamic
39
#RUN apk add --no-cache gmp-dev
40
#
41
## Copy header files needed for running LustreC
42
#COPY --from=builder /var/lustrec/include/*.h /usr/local/include/lustrec/
43
## Copy Lustrec binaries
44
#COPY --from=builder /var/lustrec/bin /lustrec/
45
#
46
#
47
#WORKDIR /lustrec
backends/.merlin
1
EXCLUDE_QUERY_DIR
2
B /home/corentin/.opam/default/lib/dune-build-info
3
B /home/corentin/.opam/default/lib/mlmpfr
4
B /home/corentin/.opam/default/lib/num
5
B /home/corentin/.opam/default/lib/ocamlgraph
6
B /home/corentin/.opam/default/lib/zarith
7
B /usr/lib/ocaml
8
B ../_build/default/backends/.backends.objs/byte
9
B ../_build/default/core/.lustrec.objs/byte
10
B ../_build/default/plugins/mpfr/.lustrec_mpfr.objs/byte
11
S /home/corentin/.opam/default/lib/dune-build-info
12
S /home/corentin/.opam/default/lib/mlmpfr
13
S /home/corentin/.opam/default/lib/num
14
S /home/corentin/.opam/default/lib/ocamlgraph
15
S /home/corentin/.opam/default/lib/zarith
16
S /usr/lib/ocaml
17
S .
18
S Ada
19
S C
20
S EMF
21
S Horn
22
S Java
23
S VHDL
24
S ../core
25
S ../core/checks
26
S ../core/features/machine_types
27
S ../core/parsers
28
S ../core/utils
29
S ../plugins/mpfr
30
FLG -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -short-paths -keep-locs -warn-error -A
backends/Ada/.merlin
1
REC
backends/Ada/README
1
This is the Ada Backend generating Ada code from the machine code computed
2
from a Lustre file.
3

  
4
The backend is split in several files described in this README.
5

  
6
=> misc_lustre_function.ml
7
Some fonction on pure Lustre machine code, no printers
8
or anything related to Ada. It just compute information from the Machine Code.
9
It contains mostly the unification code used for polymorphic type. It is
10
important since the Lustrec.Arrow node is polymorphic.
11

  
12
=> misc_printer.ml
13
Some general format printer function, not related at all
14
to Ada but used by this backend.
15

  
16
=> ada_printer.mli
17
=> ada_printer.ml
18
It contains Type representing some part of Ada syntaxe and printers function
19
to generates it. There is nothing specifics to Lustre in this file. It is
20
mostly printers for the declarative part of Ada. The printer functions takes in
21
general directly printer function build by other files(like ada_backend_common.ml)
22
to print instruction and expression contained in the declaration.
23
For example, the printer for the declaration of a variable will take
24
two printer functions as argument:
25
 - pp_type: printing the type
26
 - pp_name: printing the variable name
27
The printer will looks like :
28
--
29
let pp_var_decl pp_type pp_name =
30
  fprintf fmt "%t : %t" pp_type pp_name
31
--
32

  
33
=> ada_backend_common.mli
34
=> ada_backend_common.ml
35
It contains function printing Ada code(instruction and exression) from Machine
36
Code. This functions are used or could be used for ads and/or adb and/or
37
wrappers.
38

  
39
=> ada_backend_ads.ml
40
It contains function printing Ada code(instruction and exression) from Machine
41
Code for the Ads file.
42

  
43
=> ada_backend_adb.ml
44
It contains function printing Ada code(instruction and exression) from Machine
45
Code for the Adb file.
46

  
47
=> ada_backend_wrapper.ml
48
It contains function printing Ada code(instruction and exression) from Machine
49
Code for :
50
  - an adb file witha main function containg a loop calling step.
51
  - a project file
52
  - a configuration file
53

  
54
=> ada_backend.ml
55
It contains the main function of the backend which perform the unification
56
and write all the files using the previsous code.
57

  
58

  
backends/Ada/ada_backend.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
open Format
13
open Lustrec.Machine_code_types
14

  
15
open Misc_lustre_function
16
open Ada_printer
17
open Ada_backend_common
18

  
19
let indent_size = 2
20

  
21
(** Log at level 2 a string message with some indentation.
22
   @param indent the indentation level
23
   @param info the message
24
**)
25
let log_str_level_two indent info =
26
  let str_indent = String.make (indent*indent_size) ' ' in
27
  let pp_message fmt = fprintf fmt "%s.. %s@." str_indent info in
28
  Lustrec.Log.report ~level:2 pp_message;
29
  Format.pp_print_flush Format.err_formatter ()
30

  
31
(** Write a new file with formatter
32
   @param destname folder where the file shoudl be created
33
   @param pp_filename function printing the filename
34
   @param pp_file function wich pretty print the file
35
   @param arg will be given to pp_filename and pp_file
36
**)
37
let write_file destname pp_filename pp_file arg =
38
  let path = asprintf "%s%a" destname pp_filename arg in
39
  let out = open_out path in
40
  let fmt = formatter_of_out_channel out in
41
  log_str_level_two 2 ("generating "^path);
42
  pp_file fmt arg;
43
  pp_print_flush fmt ();
44
  close_out out
45

  
46

  
47
(** Exception raised when a machine contains a feature not supported by the
48
  Ada backend*)
49
exception CheckFailed of string
50

  
51

  
52
(** Check that a machine match the requirement for an Ada compilation :
53
      - No constants.
54
   @param machine the machine to test
55
**)
56
let check machine =
57
  match machine.mconst with
58
    | [] -> ()
59
    | _ -> raise (CheckFailed "machine.mconst should be void")
60

  
61

  
62
let get_typed_submachines machines m =
63
  let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in
64
  let submachines = List.map (get_machine machines) instances in
65
  List.map2
66
    (fun instance submachine ->
67
      let ident = (fst instance) in
68
      ident, (get_substitution m ident submachine, submachine))
69
    instances submachines
70

  
71
let extract_contract machines m =
72
  let rec find_submachine_from_ident ident = function
73
    | [] -> raise Not_found
74
    | h::t when h.mname.node_id = ident -> h
75
    | _::t -> find_submachine_from_ident ident t
76
  in
77
  let extract_ident eexpr =
78
    match eexpr.Lustrec.Lustre_types.eexpr_qfexpr.expr_desc with
79
      | Expr_ident ident -> ident
80
      | _ -> assert false
81
      (*
82
      | Expr_const cst -> assert false
83
      | Expr_tuple exprs -> assert false
84
      | Expr_ite (expr1, expr2, expr3) -> assert false
85
      | Expr_arrow (expr1, expr2)  -> assert false
86
      | Expr_fby (expr1, expr2) -> assert false
87
      | Expr_array exprs -> assert false
88
      | Expr_access (expr1, dim) -> assert false
89
      | Expr_power (expr1, dim) -> assert false
90
      | Expr_pre expr -> assert false
91
      | Expr_when (expr,ident,label) -> assert false
92
      | Expr_merge (ident, l) -> assert false
93
      | Expr_appl call -> assert false
94
      *)
95
  in
96
  match m.mspec with
97
    | Some (NodeSpec ident) ->
98
      begin
99
        let machine_spec = find_submachine_from_ident ident machines in
100
        let guarantees =
101
          match machine_spec.mspec with
102
            | Some (Contract contract) ->
103
                assert (contract.consts=[]);
104
                assert (contract.locals=[]);
105
                assert (contract.stmts=[]);
106
                assert (contract.assume=[]);
107
                List.map extract_ident contract.guarantees
108
            | _ -> assert false
109
        in
110
        let opt_machine_spec =
111
          match machine_spec.mstep.step_instrs with
112
            | [] -> None
113
            | _ -> Some machine_spec
114
        in
115
        (opt_machine_spec, guarantees)
116
      end
117
    | _ -> None, []
118

  
119
(** Main function of the Ada backend. It calls all the subfunction creating all
120
the file and fill them with Ada code representing the machines list given.
121
   @param basename name of the lustre file
122
   @param prog useless
123
   @param prog list of machines to translate
124
   @param dependencies useless
125
**)
126
let translate_to_ada basename prog machines dependencies =
127
  let module Ads = Ada_backend_ads.Main in
128
  let module Adb = Ada_backend_adb.Main in
129
  let module Wrapper = Ada_backend_wrapper.Main in
130

  
131
  let is_real_machine m =
132
    match m.mspec with
133
      | Some (Contract x) -> false
134
      | _ -> true
135
  in
136

  
137
  let filtered_machines = List.filter is_real_machine machines in
138

  
139
  let typed_submachines =
140
    List.map (get_typed_submachines machines) filtered_machines in
141
  
142
  let contracts = List.map (extract_contract machines) filtered_machines in
143

  
144
  let _machines = List.combine contracts filtered_machines in
145

  
146
  let _machines = List.combine typed_submachines _machines in
147

  
148
  let _pp_filename ext fmt (_, (_, machine)) =
149
    pp_machine_filename ext fmt machine in
150

  
151
  (* Extract the main machine if there is one *)
152
  let main_machine = (match !Lustrec.Options.main_node with
153
  | "" -> None
154
  | main_node -> (
155
    match Lustrec.Machine_code_common.get_machine_opt filtered_machines main_node with
156
    | None -> begin
157
      Format.eprintf "Ada Code generation error: %a@." Lustrec.Error.pp_error_msg Lustrec.Error.Main_not_found;
158
      raise (Lustrec.Error.Error (Lustrec.Location.dummy_loc,Lustrec.Error.Main_not_found))
159
    end
160
    | Some m -> Some m
161
  )) in
162

  
163
  let destname = !Lustrec.Options.dest_dir ^ "/" in
164

  
165
  log_str_level_two 1 "Checking machines";
166
  List.iter check machines;
167

  
168
  log_str_level_two 1 "Generating ads";
169
  List.iter (write_file destname (_pp_filename "ads") Ads.pp_file) _machines;
170

  
171
  log_str_level_two 1 "Generating adb";
172
  List.iter (write_file destname (_pp_filename "adb") Adb.pp_file) _machines;
173

  
174
  (* If a main node is given we generate a main adb file and a project file *)
175
  log_str_level_two 1 "Generating wrapper files";
176
  (match main_machine with
177
    | None -> ()
178
    | Some machine ->
179
        write_file destname pp_main_filename (Wrapper.pp_main_adb (get_typed_submachines filtered_machines machine)) machine;
180
        write_file destname (Wrapper.pp_project_name (basename^"_exe")) (Wrapper.pp_project_file filtered_machines basename) main_machine);
181
  write_file destname Wrapper.pp_project_configuration_name Wrapper.pp_project_configuration_file basename;
182
  write_file destname (Wrapper.pp_project_name (basename^"_lib")) (Wrapper.pp_project_file filtered_machines basename) None;
183

  
184

  
185
(* Local Variables: *)
186
(* compile-command:"make -C ../../.." *)
187
(* End: *)
backends/Ada/ada_backend_adb.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
open Format
13

  
14
open Lustrec.Machine_code_types
15
open Lustrec.Lustre_types
16
open Lustrec.Corelang
17
open Lustrec.Machine_code_common
18

  
19
open Misc_printer
20
open Misc_lustre_function
21
open Ada_printer
22
open Ada_backend_common
23

  
24
(** Main module for generating packages bodies
25
 **)
26
module Main =
27
struct
28

  
29
  (** Printing function for basic assignement [var := value].
30

  
31
      @param fmt the formater to print on
32
      @param var_name the name of the variable
33
      @param value the value to be assigned
34
   **)
35
  let pp_assign env fmt var value =
36
    fprintf fmt "%a := %a"
37
      (pp_var env) var
38
      (pp_value env) value
39

  
40
  (** Printing function for instruction. See
41
      {!type:Lustrec.Machine_code_types.instr_t} for more details on
42
      machine types.
43

  
44
      @param typed_submachines list of all typed machine instances of this machine
45
      @param machine the current machine
46
      @param fmt the formater to print on
47
      @param instr the instruction to print
48
   **)
49
  let rec pp_machine_instr typed_submachines env instr fmt =
50
    let pp_instr = pp_machine_instr typed_submachines env in
51
    (* Print args for a step call *)
52
    let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
53
    (* Print a when branch of a case *)
54
    let pp_when (cond, instrs) fmt =
55
      fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
56
    in
57
    (* Print a case *)
58
    let pp_case fmt (g, hl) =
59
      fprintf fmt "case %a is@,%aend case"
60
        (pp_value env) g
61
        pp_block (List.map pp_when hl)
62
    in
63
    (* Print a if *)
64
    (* If neg is true the we must test for the negation of the condition. It
65
       first check that we don't have a negation and a else case, if so it
66
       inverses the two branch and remove the negation doing a recursive
67
       call. *)
68
    let pp_if fmt (neg, g, instrs1, instrs2) =
69
      let pp_cond =
70
        if neg then
71
          fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
72
        else
73
          pp_value env
74
      in
75
      let pp_else = match instrs2 with
76
        | None -> fun fmt -> fprintf fmt ""
77
        | Some i2 -> fun fmt ->
78
            fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
79
      in
80
      fprintf fmt "if %a then@,%a%tend if"
81
        pp_cond g
82
        pp_block (List.map pp_instr instrs1)
83
        pp_else
84
    in
85
    match get_instr_desc instr with
86
      (* no reset *)
87
      | MNoReset _ -> ()
88
      (* reset  *)
89
      | MReset i when List.mem_assoc i typed_submachines ->
90
          let (substitution, submachine) = get_instance i typed_submachines in
91
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
92
          let args = if is_machine_statefull submachine then [[pp_state i]] else [] in
93
          pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
94
      | MLocalAssign (ident, value) ->
95
          pp_assign env fmt ident value
96
      | MStateAssign (ident, value) ->
97
          pp_assign env fmt ident value
98
      | MStep ([i0], i, vl) when is_builtin_fun i ->
99
          let value = mk_val (Fun (i, vl)) i0.var_type in
100
            pp_assign env fmt i0 value
101
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
102
          let (substitution, submachine) = get_instance i typed_submachines in
103
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
104
          let input = List.map (fun x fmt -> pp_value env fmt x) vl in
105
          let output = List.map pp_var_name il in
106
          let args =
107
            (if is_machine_statefull submachine then [[pp_state i]] else [])
108
              @(if input!=[] then [input] else [])
109
              @(if output!=[] then [output] else [])
110
          in
111
          pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
112
      | MBranch (_, []) -> assert false
113
      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
114
          pp_if fmt (build_if g c1 i1 tl)
115
      | MBranch (g, hl) -> pp_case fmt (g, hl)
116
      | MComment s  ->
117
          let lines = String.split_on_char '\n' s in
118
          fprintf fmt "%a" (Lustrec.Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
119
      | _ -> assert false
120

  
121
  (** Print the definition of the step procedure from a machine.
122

  
123
     @param typed_submachines list of all typed machine instances of this machine
124
     @param fmt the formater to print on
125
     @param machine the machine
126
  **)
127
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
128
    let transform_local_to_state_assign instr = match instr.instr_desc with
129
      | MLocalAssign (ident, value) -> 
130
          { instr_desc = MStateAssign (ident, value);
131
            lustre_eq= instr.lustre_eq }
132
      | x -> instr
133
    in
134
    let pp_local_ghost_list, spec_instrs = match m_spec_opt with
135
      | None -> [], []
136
      | Some m_spec ->
137
          List.map (build_pp_var_decl_local (Some (true, false, [], []))) (List.filter (fun x -> not (List.mem x.var_id guarantees)) m_spec.mstep.step_locals),
138
          List.map transform_local_to_state_assign m_spec.mstep.step_instrs
139
    in
140
    let pp_local_list = List.map (build_pp_var_decl_local None) (m.mstep.step_locals) in
141
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (m.mstep.step_instrs@spec_instrs) in
142
    let content = AdaProcedureContent ((if pp_local_ghost_list = [] then [] else [pp_local_ghost_list])@(if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
143
    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
144

  
145
  (** Print the definition of the reset procedure from a machine.
146

  
147
     @param typed_submachines list of all typed machine instances of this machine
148
     @param fmt the formater to print on
149
     @param machine the machine
150
  **)
151
  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
152
    let build_assign = function var ->
153
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
154
    in
155
    let env, memory = match m_spec_opt with
156
      | None -> env, m.mmemory
157
      | Some m_spec ->
158
          env,
159
          (m.mmemory)
160
    in
161
    let assigns = List.map build_assign memory in
162
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (assigns@m.minit) in
163
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
164

  
165
  (** Print the package definition(ads) of a machine.
166
    It requires the list of all typed instance.
167
    A typed submachine instance is (ident, type_machine) with ident
168
    the instance name and typed_machine is (substitution, machine) with machine
169
    the machine associated to the instance and substitution the instanciation of
170
    all its polymorphic types.
171
     @param fmt the formater to print on
172
     @param typed_submachines list of all typed machine instances of this machine
173
     @param m the machine
174
  **)
175
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
176
    let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
177
    let pp_reset fmt =
178
      if is_machine_statefull machine then
179
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) (machine, opt_spec_machine)
180
      else
181
        fprintf fmt ""
182
    in
183
    let aux pkgs (id, _) =
184
      try
185
        let (pkg, _) = List.assoc id ada_supported_funs in
186
        if List.mem pkg pkgs then
187
          pkgs
188
        else
189
          pkg::pkgs
190
      with Not_found -> pkgs
191
    in
192
    let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in
193
    let pp_content fmt =
194
      fprintf fmt "%t%a"
195
        (*Define the reset procedure*)
196
        pp_reset
197
        
198
        (*Define the step procedure*)
199
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine, guarantees)
200
    in
201
    fprintf fmt "%a%t%a;@."
202
      
203
      (* Include all the required packages*)
204
      (Lustrec.Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) packages
205
      (Lustrec.Utils.pp_final_char_if_non_empty ";@,@," packages)
206
      
207
      (*Print package*)
208
      (pp_package (pp_package_name machine) [] true ) pp_content
209

  
210
end
211

  
212
(* Local Variables: *)
213
(* compile-command: "make -C ../../.." *)
214
(* End: *)
backends/Ada/ada_backend_ads.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
open Format
13

  
14
open Lustrec.Machine_code_types
15
open Lustrec.Lustre_types
16
open Lustrec.Corelang
17
open Lustrec.Machine_code_common
18

  
19
open Misc_printer
20
open Misc_lustre_function
21
open Ada_printer
22
open Ada_backend_common
23

  
24

  
25

  
26
(** Functions printing the .ads file **)
27
module Main =
28
struct
29

  
30
  let rec init f = function i when i < 0 -> [] | i -> (f i)::(init f (i-1)) (*should be replaced by the init of list from ocaml std lib*)
31

  
32
  let suffixOld = "_old"
33
  let suffixNew = "_new"
34
  let pp_invariant_name fmt = fprintf fmt "inv"
35
  let pp_transition_name fmt = fprintf fmt "transition"
36
  let pp_init_name fmt = fprintf fmt "init"
37
  let pp_state_name_predicate suffix fmt = fprintf fmt "%t%s" pp_state_name suffix
38
  let pp_axiomatize_package_name fmt = fprintf  fmt "axiomatize"
39

  
40
  (** Print the expression function representing the transition predicate.
41
     @param fmt the formater to print on
42
     @param machine the machine
43
  **)
44
  let pp_init_predicate typed_submachines fmt (opt_spec_machine, m) =
45
    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
46
    pp_predicate pp_init_name [[new_state]] true fmt None
47

  
48
  (** Print the expression function representing the transition predicate.
49
     @param fmt the formater to print on
50
     @param machine the machine
51
  **)
52
  let pp_transition_predicate typed_submachines fmt (opt_spec_machine, m) =
53
    let old_state = (AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None) in
54
    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
55
    let inputs = build_pp_var_decl_step_input AdaIn None m in
56
    let outputs = build_pp_var_decl_step_output AdaIn None m in
57
    pp_predicate pp_transition_name ([[old_state; new_state]]@inputs@outputs) true fmt None
58

  
59
  let pp_invariant_predicate typed_submachines fmt (opt_spec_machine, m) =
60
    pp_predicate pp_invariant_name [[build_pp_state_decl AdaIn None]] true fmt None
61

  
62
  (** Print a new statement instantiating a generic package.
63
     @param fmt the formater to print on
64
     @param substitutions the instanciation substitution
65
     @param machine the machine to instanciate
66
  **)
67
  let pp_new_package fmt (substitutions, machine) =
68
    let pp_name = pp_package_name machine in
69
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
70
    let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
71
    pp_package_instanciation pp_new_name pp_name fmt instanciations
72

  
73
  (** Remove duplicates from a list according to a given predicate.
74
     @param eq the predicate defining equality
75
     @param l the list to parse
76
  **)
77
  let remove_duplicates eq l =
78
    let aux l x = if List.exists (eq x) l then l else x::l in
79
    List.fold_left aux [] l
80

  
81

  
82
  (** Compare two typed machines.
83
  **)
84
  let eq_typed_machine (subst1, machine1) (subst2, machine2) =
85
    (String.equal machine1.mname.node_id machine2.mname.node_id) &&
86
    (List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2)
87

  
88

  
89
  (** Print the package declaration(ads) of a machine.
90
    It requires the list of all typed instance.
91
    A typed submachine is a (ident, typed_machine) with
92
      - ident: the name 
93
      - typed_machine: a (substitution, machine) with
94
        - machine: the submachine struct
95
        - substitution the instanciation of all its polymorphic types.
96
     @param fmt the formater to print on
97
     @param typed_submachines list of all typed submachines of this machine
98
     @param m the machine
99
  **)
100
  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
101
    let typed_machines = snd (List.split typed_submachines) in
102
    let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
103
    
104
    let machines_to_import = List.map pp_package_name (snd (List.split typed_machines_set)) in
105

  
106
    let polymorphic_types = find_all_polymorphic_type m in
107
    
108
    let typed_machines_to_instanciate =
109
      List.filter (fun (l, _) -> l != []) typed_machines_set in
110

  
111
    let typed_instances = List.filter is_submachine_statefull typed_submachines in
112

  
113
    let memories = match m_spec_opt with
114
      | None -> []
115
      | Some m -> List.map (fun x-> pp_var_decl (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x)) m.mmemory
116
    in
117
    let ghost_private = memories in
118
    (* Commented since not used. Could be reinjected in the code 
119
    let vars_spec = match m_spec_opt with
120
      | None -> []
121
      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode (Some (true, false, [], []))) (m_spec.mmemory)
122
    in *)
123
    let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
124
    let states = List.map (build_pp_state_decl_from_subinstance AdaNoMode None) typed_instances in
125
    let var_lists =
126
      (if states = [] then [] else [states]) @
127
      (if vars = [] then [] else [vars]) in
128
    
129
    let pp_ifstatefull fmt pp =
130
      if is_machine_statefull m then
131
        fprintf fmt "%t" pp
132
      else
133
        fprintf fmt ""
134
    in
135

  
136
    let pp_state_decl_and_reset fmt =
137
      let init fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_init_name, [[pp_state_name]]) in
138
      let contract = Some (false, false, [], [init]) in
139
      fprintf fmt "%t;@,@,%a;@,@,"
140
        (*Declare the state type*)
141
        (pp_type_decl pp_state_type AdaPrivate)
142
        
143
        (*Declare the reset procedure*)
144
        (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract) AdaNoContent
145
    in
146

  
147
    let pp_private_section fmt =
148
      fprintf fmt "@,private@,@,%a%t%a%t%a"
149
      (*Instantiate the polymorphic type that need to be instantiated*)
150
      (Lustrec.Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
151
      (Lustrec.Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
152
      
153
      (*Define the state type*)
154
      pp_ifstatefull (fun fmt-> pp_record pp_state_type fmt var_lists)
155
        
156
      (Lustrec.Utils.pp_final_char_if_non_empty ";@,@," ghost_private)
157
      (Lustrec.Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_private
158
    in
159

  
160
    let pp_content fmt =
161
      let pp_contract_opt =
162
        let pp_var x fmt =
163
            pp_clean_ada_identifier fmt x
164
        in
165
        let guarantee_post_conditions = List.map pp_var guarantees in
166
        let state_pre_conditions, state_post_conditions =
167
          if is_machine_statefull m then
168
          begin
169
            let input = List.map pp_var_name m.mstep.step_inputs in
170
            let output = List.map pp_var_name m.mstep.step_outputs in
171
            let args =
172
              [[pp_old pp_state_name;pp_state_name]]
173
                @(if input!=[] then [input] else [])
174
                @(if output!=[] then [output] else [])
175
            in
176
            let transition fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_transition_name, args) in
177
            let invariant fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_invariant_name, [[pp_state_name]]) in
178
            [invariant], [transition;invariant]
179
          end
180
          else
181
            [], []
182
        in
183
        let post_conditions = state_post_conditions@guarantee_post_conditions in
184
        let pre_conditions = state_pre_conditions in
185
        if post_conditions = [] && pre_conditions = [] then
186
          None
187
        else
188
          Some (false, false, pre_conditions, post_conditions)
189
      in
190
      let pp_guarantee name = pp_var_decl (AdaNoMode, (fun fmt -> pp_clean_ada_identifier fmt name), pp_boolean_type , (Some (true, false, [], []))) in
191
      let ghost_public = List.map pp_guarantee guarantees in
192
      fprintf fmt "@,%a%t%a%a%a@,@,%a;@,@,%t"
193
        
194
        (Lustrec.Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_public
195
        (Lustrec.Utils.pp_final_char_if_non_empty ";@,@," ghost_public)
196
        
197
        pp_ifstatefull pp_state_decl_and_reset
198
        
199
        (*Declare the step procedure*)
200
        (pp_procedure pp_step_procedure_name (build_pp_arg_step m) pp_contract_opt) AdaNoContent
201
        
202
        pp_ifstatefull (fun fmt -> fprintf fmt ";@,")
203
        
204
        (pp_package (pp_axiomatize_package_name) [] false)
205
          (fun fmt -> fprintf fmt "pragma Annotate (GNATProve, External_Axiomatization);@,@,%a;@,%a;@,%a"
206
            (*Declare the init predicate*)
207
            (pp_init_predicate typed_submachines) (m_spec_opt, m)
208
            (*Declare the transition predicate*)
209
            (pp_transition_predicate typed_submachines) (m_spec_opt, m)
210
            (*Declare the invariant predicate*)
211
            (pp_invariant_predicate typed_submachines) (m_spec_opt, m)
212
          )
213
        
214
        (*Print the private section*)
215
        pp_private_section
216
    in
217
    
218
    let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
219
    let pp_generics = List.map pp_poly_type polymorphic_types in
220
    
221
    fprintf fmt "@[<v>%a%t%a;@]@."
222
      
223
      (* Include all the subinstance package*)
224
      (Lustrec.Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) machines_to_import
225
      (Lustrec.Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
226
      
227
      (*Begin the package*)
228
      (pp_package (pp_package_name m) pp_generics false) pp_content
229

  
230
end
backends/Ada/ada_backend_common.ml
1
open Format
2

  
3
open Lustrec.Machine_code_types
4
open Lustrec.Lustre_types
5
open Lustrec.Corelang
6
open Lustrec.Machine_code_common
7

  
8
open Ada_printer
9
open Misc_printer
10
open Misc_lustre_function
11

  
12
(** Exception for unsupported features in Ada backend **)
13
exception Ada_not_supported of string
14

  
15
(** Print the name of the state variable.
16
   @param fmt the formater to print on
17
**)
18
let pp_state_name fmt = fprintf fmt "state"
19
(** Print the type of the state variable.
20
   @param fmt the formater to print on
21
**)
22
let pp_state_type fmt = fprintf fmt "TState"
23
(** Print the name of the reset procedure
24
   @param fmt the formater to print on
25
**)
26
let pp_reset_procedure_name fmt = fprintf fmt "reset"
27
(** Print the name of the step procedure
28
   @param fmt the formater to print on
29
**)
30
let pp_step_procedure_name fmt = fprintf fmt "step"
31
(** Print the name of the main procedure.
32
   @param fmt the formater to print on
33
**)
34
let pp_main_procedure_name fmt = fprintf fmt "ada_main"
35
(** Print the name of the arrow package.
36
   @param fmt the formater to print on
37
**)
38
let pp_arrow_package_name fmt = fprintf fmt "Lustrec.Arrow"
39
(** Print the type of a polymorphic type.
40
   @param fmt the formater to print on
41
   @param id the id of the polymorphic type
42
**)
43
let pp_polymorphic_type id fmt = fprintf fmt "T_%i" id
44

  
45
let pp_past_name nbr fmt = fprintf fmt "past_state_%i" nbr
46

  
47

  
48

  
49

  
50

  
51

  
52

  
53

  
54

  
55
(*TODO Check all this function with unit test, improve this system and
56
   add support for : "cbrt", "erf", "log10", "pow", "atan2".
57
*)
58
let ada_supported_funs =
59
  [("sqrt",  ("Ada.Numerics.Elementary_Functions", "Sqrt"));
60
   ("log",   ("Ada.Numerics.Elementary_Functions", "Log"));
61
   ("exp",   ("Ada.Numerics.Elementary_Functions", "Exp"));
62
   ("pow",   ("Ada.Numerics.Elementary_Functions", "**"));
63
   ("sin",   ("Ada.Numerics.Elementary_Functions", "Sin"));
64
   ("cos",   ("Ada.Numerics.Elementary_Functions", "Cos"));
65
   ("tan",   ("Ada.Numerics.Elementary_Functions", "Tan"));
66
   ("asin",  ("Ada.Numerics.Elementary_Functions", "Arcsin"));
67
   ("acos",  ("Ada.Numerics.Elementary_Functions", "Arccos"));
68
   ("atan",  ("Ada.Numerics.Elementary_Functions", "Arctan"));
69
   ("sinh",  ("Ada.Numerics.Elementary_Functions", "Sinh"));
70
   ("cosh",  ("Ada.Numerics.Elementary_Functions", "Cosh"));
71
   ("tanh",  ("Ada.Numerics.Elementary_Functions", "Tanh"));
72
   ("asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh"));
73
   ("acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh"));
74
   ("atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh"));
75
   
76
   ("ceil",  ("", "Float'Ceiling"));
77
   ("floor", ("", "Float'Floor"));
78
   ("fmod",  ("", "Float'Remainder"));
79
   ("round", ("", "Float'Rounding"));
80
   ("trunc", ("", "Float'Truncation"));
81

  
82
   ("fabs", ("", "abs"));]
83

  
84
let is_builtin_fun ident =
85
  List.mem ident Lustrec.Basic_library.internal_funs ||
86
    List.mem_assoc ident ada_supported_funs
87

  
88
(** Print the name of a package associated to a machine.
89
   @param fmt the formater to print on
90
   @param machine the machine
91
**)
92
let pp_package_name machine fmt =
93
  if is_arrow machine then
94
      fprintf fmt "%t" pp_arrow_package_name
95
  else
96
      fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
97

  
98
(** Print a type.
99
   @param fmt the formater to print on
100
   @param type the type
101
**)
102
let pp_type fmt typ = 
103
  (match (Lustrec.Types.repr typ).Lustrec.Types.tdesc with
104
    | Lustrec.Types.Tbasic Lustrec.Types.Basic.Tint  -> pp_integer_type fmt
105
    | Lustrec.Types.Tbasic Lustrec.Types.Basic.Treal -> pp_float_type fmt
106
    | Lustrec.Types.Tbasic Lustrec.Types.Basic.Tbool -> pp_boolean_type fmt
107
    | Lustrec.Types.Tunivar                  -> pp_polymorphic_type typ.Lustrec.Types.tid fmt
108
    | Lustrec.Types.Tbasic _                 -> eprintf "Tbasic@."; assert false (*TODO*)
109
    | Lustrec.Types.Tconst _                 -> eprintf "Tconst@."; assert false (*TODO*)
110
    | Lustrec.Types.Tclock _                 -> eprintf "Tclock@."; assert false (*TODO*)
111
    | Lustrec.Types.Tarrow _                 -> eprintf "Tarrow@."; assert false (*TODO*)
112
    | Lustrec.Types.Ttuple l                 -> eprintf "Ttuple %a @." (Lustrec.Utils.fprintf_list ~sep:" " Lustrec.Types.print_ty) l; assert false (*TODO*)
113
    | Lustrec.Types.Tenum _                  -> eprintf "Tenum@.";  assert false (*TODO*)
114
    | Lustrec.Types.Tstruct _                -> eprintf "Tstruct@.";assert false (*TODO*)
115
    | Lustrec.Types.Tarray _                 -> eprintf "Tarray@."; assert false (*TODO*)
116
    | Lustrec.Types.Tstatic _                -> eprintf "Tstatic@.";assert false (*TODO*)
117
    | Lustrec.Types.Tlink _                  -> eprintf "Tlink@.";  assert false (*TODO*)
118
    | Lustrec.Types.Tvar                     -> eprintf "Tvar@.";   assert false (*TODO*)
119
    (*| _ -> eprintf "Type error : %a@." Lustrec.Types.print_ty typ; assert false *)
120
  )
121

  
122
(** Return a default ada constant for a given type.
123
   @param cst_typ the constant type
124
**)
125
let default_ada_cst cst_typ = match cst_typ with
126
  | Lustrec.Types.Basic.Tint  -> Const_int 0
127
  | Lustrec.Types.Basic.Treal -> Const_real Lustrec.Real.zero
128
  | Lustrec.Types.Basic.Tbool -> Const_tag tag_false
129
  | _ -> assert false
130

  
131
(** Make a default value from a given type.
132
   @param typ the type
133
**)
134
let mk_default_value typ =
135
  match (Lustrec.Types.repr typ).Lustrec.Types.tdesc with
136
    | Lustrec.Types.Tbasic t  -> mk_val (Cst (default_ada_cst t)) typ
137
    | _                              -> assert false (*TODO*)
138

  
139
(** Print the type of a variable.
140
   @param fmt the formater to print on
141
   @param id the variable
142
**)
143
let pp_var_type fmt id = 
144
  pp_type fmt id.var_type
145

  
146
(** Print a package name with polymorphic types specified.
147
   @param substitution correspondance between polymorphic type id and their instantiation
148
   @param fmt the formater to print on
149
   @param machine the machine
150
**)
151
let pp_package_name_with_polymorphic substitution machine fmt =
152
  let polymorphic_types = find_all_polymorphic_type machine in
153
  assert(List.length polymorphic_types = List.length substitution);
154
  let substituion = List.sort_uniq (fun x y -> fst x - fst y) substitution in
155
  assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
156
            polymorphic_types substituion);
157
  let instantiated_types = snd (List.split substitution) in
158
  fprintf fmt "%t%t%a"
159
    (pp_package_name machine)
160
    (Lustrec.Utils.pp_final_char_if_non_empty "_" instantiated_types)
161
    (Lustrec.Utils.fprintf_list ~sep:"_" pp_type) instantiated_types
162

  
163
(** Print the name of a variable.
164
   @param fmt the formater to print on
165
   @param id the variable
166
**)
167
let pp_var_name id fmt =
168
  fprintf fmt "%a" pp_clean_ada_identifier id.var_id
169

  
170
(** Print the complete name of variable.
171
   @param m the machine to check if it is memory
172
   @param fmt the formater to print on
173
   @param var the variable
174
**)
175
let pp_var env fmt var =
176
  match List.assoc_opt var.var_id env with
177
    | None -> pp_var_name var fmt
178
    | Some pp_state -> pp_access pp_state (pp_var_name var) fmt
179

  
180
(* Expression print functions *)
181

  
182
(* Printing functions for basic operations and expressions *)
183
(* TODO: refactor code -> use let rec and for basic pretty printing
184
   function *)
185
(** Printing function for Ada tags, mainly booleans.
186

  
187
    @param fmt the formater to use
188
    @param t the tag to print
189
 **)
190
let pp_ada_tag fmt t =
191
  pp_print_string fmt
192
    (if t = tag_true then "True" else if t = tag_false then "False" else t)
193

  
194
(** Printing function for machine type constants. For the moment,
195
    arrays are not supported.
196

  
197
    @param fmt the formater to use
198
    @param c the constant to print
199
 **)
200
let pp_ada_const fmt c =
201
  match c with
202
  | Const_int i                     -> pp_print_int fmt i
203
  | Const_real r                    -> Lustrec.Real.pp_ada fmt r
204
  | Const_tag t                     -> pp_ada_tag fmt t
205
  | Const_string _ | Const_modeid _ ->
206
    (Format.eprintf
207
       "internal error: Ada_backend_adb.pp_ada_const cannot print string or modeid.";
208
     assert false)
209
  | _                               ->
210
    raise (Ada_not_supported "unsupported: Ada_backend_adb.pp_ada_const does not
211
    support this constant")
212

  
213
(** Printing function for expressions [v1 modulo v2]. Depends
214
    on option [integer_div_euclidean] to choose between mathematical
215
    modulo or remainder ([rem] in Ada).
216

  
217
    @param pp_value pretty printer for values
218
    @param v1 the first value in the expression
219
    @param v2 the second value in the expression
220
    @param fmt the formater to print on
221
 **)
222
let pp_mod pp_value v1 v2 fmt =
223
  if !Lustrec.Options.integer_div_euclidean then
224
    (* (a rem b) + (a rem b < 0 ? abs(b) : 0) *)
225
    Format.fprintf fmt
226
      "((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))"
227
      pp_value v1 pp_value v2
228
      pp_value v1 pp_value v2
229
      pp_value v2
230
  else (* Ada behavior for rem *)
231
    Format.fprintf fmt "(%a rem %a)" pp_value v1 pp_value v2
232

  
233
(** Printing function for expressions [v1 div v2]. Depends on
234
    option [integer_div_euclidean] to choose between mathematic
235
    division or Ada division.
236

  
237
    @param pp_value pretty printer for values
238
    @param v1 the first value in the expression
239
    @param v2 the second value in the expression
240
    @param fmt the formater to print in
241
 **)
242
let pp_div pp_value v1 v2 fmt =
243
  if !Lustrec.Options.integer_div_euclidean then
244
    (* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *)
245
    Format.fprintf fmt "(%a - %t) / %a"
246
      pp_value v1
247
      (pp_mod pp_value v1 v2)
248
      pp_value v2
249
  else (* Ada behavior for / *)
250
    Format.fprintf fmt "(%a / %a)" pp_value v1 pp_value v2
251

  
252
(** Printing function for basic lib functions.
253

  
254
    @param pp_value pretty printer for values
255
    @param i a string representing the function
256
    @param fmt the formater to print on
257
    @param vl the list of operands
258
 **)
259
let pp_basic_lib_fun pp_value ident fmt vl =
260
  match ident, vl with
261
  | "uminus", [v]    ->
262
    Format.fprintf fmt "(- %a)" pp_value v
263
  | "not", [v]       ->
264
    Format.fprintf fmt "(not %a)" pp_value v
265
  | "impl", [v1; v2] ->
266
    Format.fprintf fmt "(not %a or else %a)" pp_value v1 pp_value v2
267
  | "=", [v1; v2]    ->
268
    Format.fprintf fmt "(%a = %a)" pp_value v1 pp_value v2
269
  | "mod", [v1; v2]  -> pp_mod pp_value v1 v2 fmt
270
  | "equi", [v1; v2] ->
271
    Format.fprintf fmt "((not %a) = (not %a))" pp_value v1 pp_value v2
272
  | "xor", [v1; v2]  ->
273
    Format.fprintf fmt "((not %a) /= (not %a))" pp_value v1 pp_value v2
274
  | "/", [v1; v2]    -> pp_div pp_value v1 v2 fmt
275
  | "&&", [v1; v2]    ->
276
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "and then" pp_value v2
277
  | "||", [v1; v2]    ->
278
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "or else" pp_value v2
279
  | "!=", [v1; v2]    ->
280
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "/=" pp_value v2
281
  | "ite", [v1; v2; v3]    ->
282
    Format.fprintf fmt "(if %a then %a else %a)" pp_value v1 pp_value v2 pp_value v3
283
  | op, [v1; v2]     ->
284
    Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
285
  | op, [v1] when  List.mem_assoc ident ada_supported_funs ->
286
    let pkg, name = try List.assoc ident ada_supported_funs
287
      with Not_found -> assert false in
288
    let pkg = pkg^(if String.equal pkg "" then "" else ".") in
289
      Format.fprintf fmt "%s%s(%a)" pkg name pp_value v1
290
  | fun_name, _      ->
291
    (Format.eprintf "internal compilation error: basic function %s@." fun_name; assert false)
292

  
293
(** Printing function for values.
294

  
295
    @param m the machine to know the state variable
296
    @param fmt the formater to use
297
    @param value the value to print. Should be a
298
           {!type:Lustrec.Machine_code_types.value_t} value
299
 **)
300
let rec pp_value env fmt value =
301
  match value.value_desc with
302
  | Cst c             -> pp_ada_const fmt c
303
  | Var var      -> pp_var env fmt var (* Find better to test if it is memory or not *)
304
  | Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value env) f_ident fmt vl
305
  | _                 ->
306
    raise (Ada_not_supported
307
             "unsupported: Ada_backend.adb.pp_value does not support this value type")
308

  
309

  
310
(** Print the filename of a machine package.
311
   @param extension the extension to append to the package name
312
   @param fmt the formatter
313
   @param machine the machine corresponding to the package
314
**)
315
let pp_machine_filename extension fmt machine =
316
  pp_filename extension fmt (pp_package_name machine)
317

  
318
let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name
319

  
320

  
321
(** Print the declaration of a state element of a subinstance of a machine.
322
   @param machine the machine
323
   @param fmt the formater to print on
324
   @param substitution correspondance between polymorphic type id and their instantiation
325
   @param ident the identifier of the subinstance
326
   @param submachine the submachine of the subinstance
327
**)
328
let build_pp_state_decl_from_subinstance mode with_statement (name, (substitution, machine)) =
329
  let pp_package = pp_package_name_with_polymorphic substitution machine in
330
  let pp_type = pp_package_access (pp_package, pp_state_type) in
331
  let pp_name fmt = pp_clean_ada_identifier fmt name in
332
  (mode, pp_name, pp_type, with_statement)
333

  
334
(** Print variable declaration for a local state variable
335
   @param fmt the formater to print on
336
   @param mode input/output mode of the parameter
337
**)
338
let build_pp_state_decl mode with_statement =
339
  (mode, pp_state_name, pp_state_type, with_statement)
340

  
341
let build_pp_var_decl mode with_statement var =
342
  let pp_name = function fmt -> pp_var_name var fmt in
343
  let pp_type = function fmt -> pp_var_type fmt var in
344
  (mode, pp_name, pp_type, with_statement)
345

  
346
let build_pp_var_decl_local with_statement var =
347
  AdaLocalVar (build_pp_var_decl AdaNoMode with_statement var)
348

  
349
let build_pp_var_decl_step_input mode with_statement m =
350
  if m.mstep.step_inputs=[] then [] else
351
    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_inputs]
352

  
353
let build_pp_var_decl_step_output mode with_statement m =
354
  if m.mstep.step_outputs=[] then [] else
355
    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_outputs]
356

  
357
let build_pp_var_decl_static mode with_statement m =
358
  if m.mstatic=[] then [] else
359
    [List.map (build_pp_var_decl mode with_statement) m.mstatic]
360

  
361
let build_pp_arg_step m =
362
  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
363
    @ (build_pp_var_decl_step_input AdaIn None m)
364
    @ (build_pp_var_decl_step_output AdaOut None m)
365

  
366
let build_pp_arg_reset m =
367
  (if is_machine_statefull m then [[build_pp_state_decl AdaOut None]] else [])
368
    @ (build_pp_var_decl_static AdaIn None m)
369

  
370

  
371
let build_pp_arg_transition m =
372
  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
373
    @ (build_pp_var_decl_step_input AdaIn None m)
374
    @ (build_pp_var_decl_step_output AdaOut None m)
375

  
backends/Ada/ada_backend_common.mli
1
open Format
2

  
3
open Lustrec.Machine_code_types
4
open Lustrec.Lustre_types
5
open Lustrec.Types
6

  
7
open Ada_printer
8
open Misc_printer
9

  
10
val pp_state_name : printer
11
val pp_state_type : printer
12
val pp_reset_procedure_name : printer
13
val pp_step_procedure_name : printer
14
val pp_main_procedure_name : printer
15
val pp_polymorphic_type : int -> printer
16
val pp_past_name : int -> printer
17

  
18
val is_builtin_fun : string -> bool
19
val ada_supported_funs : (string*(string*string)) list
20

  
21
val pp_var_name : var_decl -> formatter -> unit
22
val pp_var : ((string*printer) list) -> formatter -> var_decl -> unit
23
val pp_value : ((string*printer) list) -> formatter -> value_t -> unit
24
val pp_type : formatter -> type_expr -> unit
25
val pp_var_type : formatter -> var_decl -> unit
26

  
27
val pp_package_name : machine_t -> printer
28
val pp_package_name_with_polymorphic : (int * Lustrec.Types.type_expr) list -> machine_t -> printer
29

  
30
val mk_default_value : type_expr -> value_t
31

  
32
val build_pp_var_decl : parameter_mode -> ada_with -> var_decl -> ada_var_decl
33
val build_pp_var_decl_local : ada_with -> var_decl -> ada_local_decl
34
val build_pp_var_decl_step_input : parameter_mode -> ada_with -> machine_t -> (ada_var_decl list list)
35
val build_pp_var_decl_step_output : parameter_mode -> ada_with -> machine_t -> (ada_var_decl list list)
36
val build_pp_arg_step : machine_t -> (ada_var_decl list list)
37
val build_pp_arg_reset : machine_t -> (ada_var_decl list list)
38
val build_pp_state_decl_from_subinstance : parameter_mode -> ada_with -> (string * ((int * Lustrec.Types.type_expr) list * Lustrec.Machine_code_types.machine_t)) -> ada_var_decl
39
val build_pp_state_decl : parameter_mode -> ada_with -> ada_var_decl
40

  
41
val pp_machine_filename : string -> formatter -> machine_t -> unit
42
val pp_main_filename : formatter -> machine_t -> unit
backends/Ada/ada_backend_wrapper.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
open Format
13

  
14
open Lustrec.Machine_code_types
15
open Lustrec.Lustre_types
16

  
17
open Misc_printer
18
open Misc_lustre_function
19
open Ada_printer
20
open Ada_backend_common
21

  
22
module Main =
23
struct
24

  
25
  let build_text_io_package_local typ =
26
    AdaLocalPackage (
27
      (fun fmt -> fprintf fmt "%s_IO" typ),
28
      (fun fmt -> fprintf fmt "Ada.Text_IO.%s_IO" typ),
29
      [((fun fmt -> fprintf fmt "Num"), (fun fmt -> fprintf fmt "%s" typ))])
30

  
31
  (** Print the main file calling in a loop the step function of the main machine.
32
     @param fmt the formater to print on
33
     @param machine the main machine
34
  **)
35
  let pp_main_adb typed_submachines fmt machine =
36
    let statefull = is_machine_statefull machine in
37
    
38
    let pp_package = pp_package_name_with_polymorphic [] machine in
39
    
40
    (* Dependances *)
41
    let text_io = "Ada.Text_IO" in
42
    
43
    (* Locals *)
44
    let locals =
45
      [[build_text_io_package_local "Integer";build_text_io_package_local "Float"]]
46
      @(if statefull then [[AdaLocalVar (build_pp_state_decl_from_subinstance AdaNoMode None (asprintf "%t" pp_state_name, ([], machine)))]] else [])
47
      @(if machine.mstep.step_inputs != [] then [List.map (build_pp_var_decl_local None) machine.mstep.step_inputs] else [])
48
      @(if machine.mstep.step_outputs != [] then [List.map (build_pp_var_decl_local None) machine.mstep.step_outputs] else [])
49
    in
50

  
51
    (* Stream instructions *)
52
    let get_basic var = match (Lustrec.Types.repr var.var_type ).Lustrec.Types.tdesc with
53
        Lustrec.Types.Tbasic x -> x | _ -> assert false in
54
    let pp_read fmt var =
55
      match get_basic var with
56
        | Lustrec.Types.Basic.Tbool ->
57
            fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
58
              (pp_var_name var)
59
        | _ ->
60
            fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)"
61
              (pp_var_name var)
62
              pp_var_type var
63
    in
64
    let pp_write fmt var =
65
      match get_basic var with
66
        | Lustrec.Types.Basic.Tbool ->
67
            fprintf fmt "Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \"' \")"
68
              (pp_var_name var)
69
              (pp_var_name var)
70
        | Lustrec.Types.Basic.Tint ->
71
            fprintf fmt "Ada.Text_IO.Put(\"'%t': '\");@,Integer_IO.Put(%t);@,Ada.Text_IO.Put_Line(\"' \")"
72
              (pp_var_name var)
73
              (pp_var_name var)
74
        | Lustrec.Types.Basic.Treal ->
75
            fprintf fmt "Ada.Text_IO.Put(\"'%t': '\");@,Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,Ada.Text_IO.Put_Line(\"' \")"
76
              (pp_var_name var)
77
              (pp_var_name var)
78
        | Lustrec.Types.Basic.Tstring | Lustrec.Types.Basic.Trat -> assert false (* Could not be the top level inputs *)
79
    in
80

  
81
    (* Loop instructions *)
82
    let pp_loop fmt =
83
      let args = pp_state_name::(List.map pp_var_name (machine.mstep.step_inputs@machine.mstep.step_outputs)) in
84
      fprintf fmt "while not Ada.Text_IO.End_Of_File loop@,  @[<v>%a;@,%a;@,%a;@]@,end loop"
85
        (Lustrec.Utils.fprintf_list ~sep:";@," pp_read) machine.mstep.step_inputs
86
        pp_call (pp_package_access (pp_package, pp_step_procedure_name), [args])
87
        (Lustrec.Utils.fprintf_list ~sep:";@," pp_write) machine.mstep.step_outputs in
88
    
89
    (* Print the file *)
90
    let instrs = (if statefull then [fun fmt -> pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), [[pp_state_name]])] else [])@[pp_loop] in
91
    fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]"
92
      (pp_with AdaPrivate) (pp_str text_io)
93
      (pp_with AdaPrivate) (pp_package_name machine)
94
      (pp_procedure pp_main_procedure_name [] None) (AdaProcedureContent (locals, instrs))
95

  
96
  (** Print the name of the ada project configuration file.
97
     @param fmt the formater to print on
98
     @param main_machine the machine associated to the main node
99
  **)
100
  let pp_project_configuration_name fmt basename =
101
    fprintf fmt "%s.adc" basename
102

  
103
  (** Print the project configuration file.
104
     @param fmt the formater to print on
105
     @param machine the main machine
106
  **)
107
  let pp_project_configuration_file fmt machine =
108
    fprintf fmt "pragma SPARK_Mode (On);"
109

  
110
  (** Print the name of the ada project file.
111
     @param base_name name of the lustre file
112
     @param fmt the formater to print on
113
     @param machine_opt the main machine option
114
  **)
115
  let pp_project_name basename fmt machine_opt =
116
    fprintf fmt "%s.gpr" basename
117

  
118
  let pp_for_single name arg fmt =
119
    fprintf fmt "for %s use \"%s\"" name arg
120

  
121
  let pp_for name args fmt =
122
    fprintf fmt "for %s use (@[%a@])" name
123
      (Lustrec.Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg))
124
      args
125

  
126
  let pp_content fmt lines =
127
    fprintf fmt "  @[<v>%a%t@]"
128
      (Lustrec.Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) lines
129
      (Lustrec.Utils.pp_final_char_if_non_empty ";" lines)
130

  
131
  let pp_package name lines fmt =
132
    fprintf fmt "package %s is@,%a@,end %s"
133
      name
134
      pp_content lines
135
      name
136

  
137
  (** Print the gpr project file, if there is a machine in machine_opt then
138
        an executable project is made else it is a library.
139
     @param fmt the formater to print on
140
     @param machine_opt the main machine option
141
  **)
142
  let pp_project_file machines basename fmt machine_opt =
143
    let adbs = (List.map (asprintf "%a" (pp_machine_filename "adb")) machines)
144
                  @(match machine_opt with
145
                    | None -> []
146
                    | Some m -> [asprintf "%a" pp_main_filename m]) in
147
    let project_name = basename^(if machine_opt=None then "_lib" else "_exe") in
148
    fprintf fmt "%sproject %s is@,%a@,end %s;" (if machine_opt=None then "library " else "") project_name
149
    pp_content
150
    ((match machine_opt with
151
      | None -> [
152
          pp_for_single "Library_Name" basename;
153
          pp_for_single "Library_Dir" "lib";
154
        ]
155
      | Some machine -> [
156
          pp_for "Main" [asprintf "%t" pp_main_procedure_name];
157
          pp_for_single "Exec_Dir" "bin";
158
        ])
159
    @[
160
      pp_for_single "Object_Dir" "obj";
161
      pp_for "Source_Files" adbs;
162
      pp_package "Builder" [
163
        pp_for_single "Lustrec.Global_Configuration_Pragmas" (asprintf "%a" pp_project_configuration_name basename);
164
      ];
165
      pp_package "Prove" [
166
        pp_for "Switches" ["--mode=prove"; "--report=statistics"; "--proof=per_check"; "--warnings=continue"];
167
        pp_for_single "Proof_Dir" (asprintf "proof");
168
      ]
169
    ])
170
    project_name
171

  
172

  
173
  end
backends/Ada/ada_printer.ml
1
open Format
2

  
3
(** Represent the possible mode for a type of a procedure parameter **)
4
type parameter_mode = AdaNoMode | AdaIn | AdaOut | AdaInOut
5

  
6
type kind_def = AdaType | AdaProcedure | AdaFunction | AdaPackageDecl | AdaPackageBody
7

  
8
type visibility = AdaNoVisibility | AdaPrivate | AdaLimitedPrivate
9

  
10
type printer = Format.formatter -> unit
11

  
12
type ada_with = (bool * bool * (printer list) * (printer list)) option
13

  
14
type ada_var_decl = parameter_mode * printer * printer * ada_with
15

  
16
type ada_local_decl =
17
  | AdaLocalVar of ada_var_decl
18
  | AdaLocalPackage of (printer * printer * ((printer*printer) list))
19

  
20
type def_content =
21
  | AdaNoContent
22
  | AdaPackageContent of printer
23
  | AdaSimpleContent of printer
24
  | AdaVisibilityDefinition of visibility
25
  | AdaProcedureContent of ((ada_local_decl list list) * (printer list))
26
  | AdaRecord of ((ada_var_decl list) list)
27
  | AdaPackageInstanciation of (printer * (printer * printer) list)
28

  
29
(** Print a parameter_mode.
30
   @param fmt the formater to print on
31
   @param mode the modifier
32
**)
33
let pp_parameter_mode fmt mode =
34
  fprintf fmt "%s" (match mode with
35
                     | AdaNoMode -> ""
36
                     | AdaIn     -> "in"
37
                     | AdaOut    -> "out"
38
                     | AdaInOut  -> "in out")
39

  
40
let pp_kind_def fmt kind_def =
41
  fprintf fmt "%s" (match kind_def with
42
                     | AdaType        -> "type"
43
                     | AdaProcedure   -> "procedure"
44
                     | AdaFunction    -> "function"
45
                     | AdaPackageDecl -> "package"
46
                     | AdaPackageBody -> "package body")
47

  
48
let pp_visibility fmt visibility =
49
  fprintf fmt "%s" (match visibility with
50
                     | AdaNoVisibility     -> ""
51
                     | AdaPrivate          -> "private"
52
                     | AdaLimitedPrivate   -> "limited private")
53

  
54
(** Print the integer type name.
55
   @param fmt the formater to print on
56
**)
57
let pp_integer_type fmt = fprintf fmt "Integer"
58

  
59
(** Print the float type name.
60
   @param fmt the formater to print on
61
**)
62
let pp_float_type fmt = fprintf fmt "Float"
63

  
64
(** Print the boolean type name.
65
   @param fmt the formater to print on
66
**)
67
let pp_boolean_type fmt = fprintf fmt "Boolean"
68

  
69
let pp_group ~sep:sep pp_list fmt =
70
  assert(pp_list != []);
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff