Project

General

Profile

« Previous | Next » 

Revision 61e0c3c4

Added by Guillaume DAVY about 4 years ago

Ada:
- Correct the merge with lustrec-seal
- Improve support for builtin function(still work to do)
- Add generation of a gpr file for lib(without main).
- Add var initialisation in the reset, still work to do.

View differences:

src/backends/Ada/ada_backend.ml
42 42
  close_out out
43 43

  
44 44

  
45
(** Print the filename of a machine package.
46
   @param extension the extension to append to the package name
47
   @param fmt the formatter
48
   @param machine the machine corresponding to the package
49
**)
50
let pp_machine_filename extension fmt machine =
51
  pp_filename extension fmt (function fmt -> pp_package_name fmt machine)
52

  
53 45
(** Exception raised when a machine contains a feature not supported by the
54 46
  Ada backend*)
55 47
exception CheckFailed of string
......
64 56
    | [] -> ()
65 57
    | _ -> raise (CheckFailed "machine.mconst should be void")
66 58

  
67
(** Print the name of the ada project file.
68
   @param fmt the formater to print on
69
   @param main_machine the machine associated to the main node
70
**)
71
let pp_project_name fmt main_machine =
72
  fprintf fmt "%a.gpr" pp_package_name main_machine
73

  
74 59

  
75 60
let get_typed_submachines machines m =
76 61
  let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in
......
83 68

  
84 69
(** Main function of the Ada backend. It calls all the subfunction creating all
85 70
the file and fill them with Ada code representing the machines list given.
86
   @param basename useless
71
   @param basename name of the lustre file
87 72
   @param prog useless
88 73
   @param prog list of machines to translate
89 74
   @param dependencies useless
......
98 83

  
99 84
  let _machines = List.combine typed_submachines machines in
100 85

  
101
  let _pp_filename ext fmt (typed_submachines, machine) =
86
  let _pp_filename ext fmt (typed_submachine, machine) =
102 87
    pp_machine_filename ext fmt machine in
103 88

  
104 89
  (* Extract the main machine if there is one *)
......
126 111

  
127 112
  (* If a main node is given we generate a main adb file and a project file *)
128 113
  log_str_level_two 1 "Generating wrapper files";
129
  match main_machine with
130
    | None -> log_str_level_two 2 "File not generated(no -node argument)";
114
  (match main_machine with
115
    | None -> ()
131 116
    | Some machine ->
132
begin
133
  let pp_main_filename fmt _ =
134
    pp_filename "adb" fmt pp_main_procedure_name in
135
  write_file destname pp_project_name Wrapper.pp_project_file machine;
136
  write_file destname pp_main_filename Wrapper.pp_main_adb machine;
137
end
117
        write_file destname pp_main_filename Wrapper.pp_main_adb machine;
118
        write_file destname (Wrapper.pp_project_name (basename^"_exe")) (Wrapper.pp_project_file machines basename) main_machine);
119
  write_file destname Wrapper.pp_project_configuration_name Wrapper.pp_project_configuration_file basename;
120
  write_file destname (Wrapper.pp_project_name (basename^"_lib")) (Wrapper.pp_project_file machines basename) None;
138 121

  
139 122

  
140 123
(* Local Variables: *)
src/backends/Ada/ada_backend_adb.ml
170 170
     @param fmt the formater to print on
171 171
     @param machine the machine
172 172
  **)
173
  let pp_step_definition typed_submachines fmt m = pp_procedure_definition
174
        pp_step_procedure_name
175
        (pp_step_prototype m)
176
        (pp_machine_var_decl NoMode)
177
        (pp_machine_instr typed_submachines m)
178
        fmt
179
        (m.mstep.step_locals, m.mstep.step_instrs)
173
  let pp_step_definition typed_submachines fmt m =
174
    pp_procedure_definition
175
      pp_step_procedure_name
176
      (pp_step_prototype m)
177
      (pp_machine_var_decl NoMode)
178
      (pp_machine_instr typed_submachines m)
179
      fmt
180
      (m.mstep.step_locals, m.mstep.step_instrs)
180 181

  
181 182
  (** Print the definition of the reset procedure from a machine.
182 183

  
......
184 185
     @param fmt the formater to print on
185 186
     @param machine the machine
186 187
  **)
187
  let pp_reset_definition typed_submachines fmt m = pp_procedure_definition
188
        pp_reset_procedure_name
189
        (pp_reset_prototype m)
190
        (pp_machine_var_decl NoMode)
191
        (pp_machine_instr typed_submachines m)
192
        fmt
193
        ([], m.minit)
188
  let pp_reset_definition typed_submachines fmt m =
189
    let build_assign = function var ->
190
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
191
    in
192
    let assigns = List.map build_assign m.mmemory in
193
    pp_procedure_definition
194
      pp_reset_procedure_name
195
      (pp_reset_prototype m)
196
      (pp_machine_var_decl NoMode)
197
      (pp_machine_instr typed_submachines m)
198
      fmt
199
      ([], assigns@m.minit)
194 200

  
195 201
  (** Print the package definition(ads) of a machine.
196 202
    It requires the list of all typed instance.
src/backends/Ada/ada_backend_ads.ml
106 106
  let pp_procedure_prototype_contract pp_prototype fmt opt_contract =
107 107
    match opt_contract with
108 108
      | None -> pp_prototype fmt
109
      | Some contract -> 
110
          fprintf fmt "@[<v 2>%t with@,%a%t%a@]"
109
      | Some (NodeSpec ident) -> pp_prototype fmt (*TODO*)
110
      | Some (Contract contract) ->
111
          fprintf fmt "@[<v 2>%t with@,Global => null;@,%a%t%a@]"
111 112
            pp_prototype
112 113
            (Utils.fprintf_list ~sep:",@," pp_pre) contract.assume
113 114
            (Utils.pp_final_char_if_non_empty ",@," contract.assume)
......
118 119
     @param machine the machine
119 120
  **)
120 121
  let pp_step_prototype_contract fmt m =
121
    ()
122
      (* Temporarily disabled while waiting for the code to stabilize 
123
pp_procedure_prototype_contract
124
        (pp_step_prototype m)
125
        fmt
126
        m.mspec
127
       *)
122
    pp_procedure_prototype_contract
123
      (pp_step_prototype m)
124
      fmt
125
      m.mspec
126
       
128 127
    
129 128
  (** Remove duplicates from a list according to a given predicate.
130 129
     @param eq the predicate defining equality
src/backends/Ada/ada_backend_common.ml
14 14

  
15 15
let is_machine_statefull m = not m.mname.node_dec_stateless
16 16

  
17
(*TODO Check all this function with unit test, improve this system and
18
   add support for : "cbrt", "erf", "log10", "pow", "atan2".
19
*)
17 20
let ada_supported_funs =
18
  [("sin", ("Ada.Numerics.Elementary_Functions", "Sin"));
19
   ("cos", ("Ada.Numerics.Elementary_Functions", "Cos"));
20
   ("tan", ("Ada.Numerics.Elementary_Functions", "Tan"))]
21
  [("sqrt",  ("Ada.Numerics.Elementary_Functions", "Sqrt"));
22
   ("log",   ("Ada.Numerics.Elementary_Functions", "Log"));
23
   ("exp",   ("Ada.Numerics.Elementary_Functions", "Exp"));
24
   ("pow",   ("Ada.Numerics.Elementary_Functions", "**"));
25
   ("sin",   ("Ada.Numerics.Elementary_Functions", "Sin"));
26
   ("cos",   ("Ada.Numerics.Elementary_Functions", "Cos"));
27
   ("tan",   ("Ada.Numerics.Elementary_Functions", "Tan"));
28
   ("asin",  ("Ada.Numerics.Elementary_Functions", "Arcsin"));
29
   ("acos",  ("Ada.Numerics.Elementary_Functions", "Arccos"));
30
   ("atan",  ("Ada.Numerics.Elementary_Functions", "Arctan"));
31
   ("sinh",  ("Ada.Numerics.Elementary_Functions", "Sinh"));
32
   ("cosh",  ("Ada.Numerics.Elementary_Functions", "Cosh"));
33
   ("tanh",  ("Ada.Numerics.Elementary_Functions", "Tanh"));
34
   ("asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh"));
35
   ("acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh"));
36
   ("atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh"));
37
   
38
   ("ceil",  ("", "Float'Ceiling"));
39
   ("floor", ("", "Float'Floor"));
40
   ("fmod",  ("", "Float'Remainder"));
41
   ("round", ("", "Float'Rounding"));
42
   ("trunc", ("", "Float'Truncation"));
43

  
44
   ("fabs", ("", "abs"));]
21 45

  
22 46
let is_builtin_fun ident =
23 47
  List.mem ident Basic_library.internal_funs ||
......
82 106

  
83 107
(* Package pretty print functions *)
84 108

  
109
(** Return true if its the arrow machine
110
   @param machine the machine to test
111
*)
112
let is_arrow machine = String.equal Arrow.arrow_id machine.mname.node_id
113

  
85 114
(** Print the name of the arrow package.
86 115
   @param fmt the formater to print on
87 116
**)
88 117
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
89 118

  
90
(** Print the name of a package associated to a node.
91
   @param fmt the formater to print on
92
   @param machine the machine
93
**)
94
let pp_package_name_from_node fmt node =
95
  if String.equal Arrow.arrow_id node.node_id then
96
      fprintf fmt "%t" pp_arrow_package_name
97
  else
98
      fprintf fmt "%a" pp_clean_ada_identifier node.node_id
99

  
100 119
(** Print the name of a package associated to a machine.
101 120
   @param fmt the formater to print on
102 121
   @param machine the machine
103 122
**)
104 123
let pp_package_name fmt machine =
105
  pp_package_name_from_node fmt machine.mname
124
  if is_arrow machine then
125
      fprintf fmt "%t" pp_arrow_package_name
126
  else
127
      fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
106 128

  
107 129
(** Print the ada package introduction sentence it can be used for body and
108 130
declaration. Boolean parameter body should be true if it is a body delcaration.
......
177 199
    try
178 200
      List.find (function m -> m.mname.node_id=id) machines
179 201
    with
180
      Not_found -> assert false
202
      Not_found -> assert false (*TODO*)
181 203

  
182 204

  
183 205
(* Type pretty print functions *)
......
246 268
    | Types.Tbasic Types.Basic.Tint  -> pp_integer_type fmt
247 269
    | Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
248 270
    | Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
249
    | Types.Tunivar                  -> pp_polymorphic_type fmt typ.tid
271
    | Types.Tunivar                  -> pp_polymorphic_type fmt typ.Types.tid
250 272
    | Types.Tbasic _                 -> eprintf "Tbasic@."; assert false (*TODO*)
251 273
    | Types.Tconst _                 -> eprintf "Tconst@."; assert false (*TODO*)
252 274
    | Types.Tclock _                 -> eprintf "Tclock@."; assert false (*TODO*)
......
261 283
    (*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *)
262 284
  )
263 285

  
286
(** Return a default ada constant for a given type.
287
   @param cst_typ the constant type
288
**)
289
let default_ada_cst cst_typ = match cst_typ with
290
  | Types.Basic.Tint  -> Const_int 0
291
  | Types.Basic.Treal -> Const_real (Num.num_of_int 0, 0, "0.0")
292
  | Types.Basic.Tbool -> Const_tag tag_false
293

  
294
(** Make a default value from a given type.
295
   @param typ the type
296
**)
297
let mk_default_value typ =
298
  match (Types.repr typ).Types.tdesc with
299
    | Types.Tbasic t  -> mk_val (Cst (default_ada_cst t)) typ
300
    | _                              -> assert false (*TODO*)
264 301

  
265 302
(** Test if two types are the same.
266 303
   @param typ1 the first type
......
472 509
   @param pp_name name function printer
473 510
**)
474 511
let pp_reset_prototype m fmt =
475
  let state_mode = if is_machine_statefull m then Some InOut else None in
512
  let state_mode = if is_machine_statefull m then Some Out else None in
476 513
  pp_base_prototype state_mode m.mstatic [] fmt pp_reset_procedure_name
477 514

  
478 515
(** Print the prototype of the init procedure of a machine.
......
685 722
  let pp_ada_const fmt c =
686 723
    match c with
687 724
    | Const_int i                     -> pp_print_int fmt i
688
    | Const_real (c, e, s)            -> pp_print_string fmt s
725
    | Const_real (c, e, s)            ->
726
        fprintf fmt "%s.0*1.0e-%i" (Num.string_of_num c) e
689 727
    | Const_tag t                     -> pp_ada_tag fmt t
690 728
    | Const_string _ | Const_modeid _ ->
691 729
      (Format.eprintf
......
788 826
    | _                 ->
789 827
      raise (Ada_not_supported
790 828
               "unsupported: Ada_backend.adb.pp_value does not support this value type")
829

  
830

  
831
(** Print the filename of a machine package.
832
   @param extension the extension to append to the package name
833
   @param fmt the formatter
834
   @param machine the machine corresponding to the package
835
**)
836
let pp_machine_filename extension fmt machine =
837
  pp_filename extension fmt (function fmt -> pp_package_name fmt machine)
838

  
839
let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name
src/backends/Ada/ada_backend_wrapper.ml
49 49
     @param machine the main machine
50 50
  **)
51 51
  let pp_main_adb fmt machine =
52
    let pp_str str fmt = fprintf fmt "%s"str in
52
    let pp_str str fmt = fprintf fmt "%s" str in
53 53
    (* Dependances *)
54 54
    let text_io = "Ada.Text_IO" in
55 55
    let float_io = "package Float_IO is new Ada.Text_IO.Float_IO(Float)" in
......
119 119
      pp_with_machine machine
120 120
      (pp_main_procedure_definition machine) (locals, instrs)
121 121

  
122
  (** Print the gpr project file.
122
  (** Print the name of the ada project configuration file.
123
     @param fmt the formater to print on
124
     @param main_machine the machine associated to the main node
125
  **)
126
  let pp_project_configuration_name fmt basename =
127
    fprintf fmt "%s.adc" basename
128

  
129
  (** Print the project configuration file.
123 130
     @param fmt the formater to print on
124 131
     @param machine the main machine
125 132
  **)
126
  let pp_project_file fmt machine =
127
      fprintf fmt "project %a is@.  for Main use (\"%a\");@.end %a;"
128
        pp_package_name machine
129
        (pp_filename "adb") pp_main_procedure_name
130
        pp_package_name machine
133
  let pp_project_configuration_file fmt machine =
134
    fprintf fmt "pragma SPARK_Mode (On);"
135

  
136
  (** Print the name of the ada project file.
137
     @param base_name name of the lustre file
138
     @param fmt the formater to print on
139
     @param machine_opt the main machine option
140
  **)
141
  let pp_project_name basename fmt machine_opt =
142
    fprintf fmt "%s.gpr" basename
143

  
144
  let pp_for_single name arg fmt =
145
    fprintf fmt "for %s use \"%s\"" name arg
146

  
147
  let pp_for name args fmt =
148
    fprintf fmt "for %s use (@[%a@])" name
149
      (Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg))
150
      args
151

  
152
  let pp_content fmt lines =
153
    fprintf fmt "  @[<v>%a%t@]"
154
      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) lines
155
      (Utils.pp_final_char_if_non_empty ";" lines)
156

  
157
  let pp_package name lines fmt =
158
    fprintf fmt "package %s is@,%a@,end %s"
159
      name
160
      pp_content lines
161
      name
162

  
163
  (** Print the gpr project file, if there is a machine in machine_opt then
164
        an executable project is made else it is a library.
165
     @param fmt the formater to print on
166
     @param machine_opt the main machine option
167
  **)
168
  let pp_project_file machines basename fmt machine_opt =
169
    let adbs = (List.map (asprintf "%a" (pp_machine_filename "adb")) machines)
170
                  @(match machine_opt with
171
                    | None -> []
172
                    | Some m -> [asprintf "%a" pp_main_filename m]) in
173
    let project_name = basename^(if machine_opt=None then "_lib" else "_exe") in
174
    fprintf fmt "%sproject %s is@,%a@,end %s;" (if machine_opt=None then "library " else "") project_name
175
    pp_content
176
    ((match machine_opt with
177
      | None -> [
178
          pp_for_single "Library_Name" basename;
179
          pp_for_single "Library_Dir" "lib";
180
        ]
181
      | Some machine -> [
182
          pp_for "Main" [asprintf "%t" pp_main_procedure_name];
183
          pp_for_single "Exec_Dir" "bin";
184
        ])
185
    @[
186
      pp_for_single "Object_Dir" "obj";
187
      pp_for "Source_Files" adbs;
188
      pp_package "Builder" [
189
        pp_for_single "Global_Configuration_Pragmas" (asprintf "%a" pp_project_configuration_name basename);
190
      ];
191
      pp_package "Prove" [
192
        pp_for "Switches" ["--mode=prove"; "--report=statistics"; "--proof=per_check"; "--warnings=continue"];
193
      ]
194
    ])
195
    project_name
196

  
131 197

  
132 198
  end

Also available in: Unified diff