Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / mpfr.ml @ 8446bf03

History | View | Annotate | Download (8.56 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
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 Utils
13
open Lustre_types
14
open Machine_code_types
15
open Corelang
16
open Normalization
17
open Machine_code
18

    
19
let mpfr_module = mktop (Open(false, "mpfr_lustre"))
20

    
21
let mpfr_rnd () = "MPFR_RNDN"
22

    
23
let mpfr_prec () = !Options.mpfr_prec
24

    
25
let inject_id = "MPFRId"
26

    
27
let inject_copy_id = "mpfr_set"
28

    
29
let inject_real_id = "mpfr_set_flt"
30

    
31
let inject_init_id = "mpfr_init2"
32

    
33
let inject_clear_id = "mpfr_clear"
34

    
35
let mpfr_t = "mpfr_t"
36

    
37
let unfoldable_value value =
38
  not (Types.is_real_type value.value_type && is_const_value value)
39

    
40
let inject_id_id expr =
41
  let e = mkpredef_call expr.expr_loc inject_id [expr] in
42
  { e with
43
    expr_type = Type_predef.type_real;
44
    expr_clock = expr.expr_clock;
45
  }
46

    
47
let pp_inject_real pp_var pp_val fmt var value =
48
  Format.fprintf fmt "%s(%a, %a, %s);"
49
    inject_real_id
50
    pp_var var
51
    pp_val value
52
    (mpfr_rnd ())
53

    
54
let inject_assign expr =
55
  let e = mkpredef_call expr.expr_loc inject_copy_id [expr] in
56
  { e with
57
    expr_type = Type_predef.type_real;
58
    expr_clock = expr.expr_clock;
59
  }
60

    
61
let pp_inject_copy pp_var fmt var value =
62
  Format.fprintf fmt "%s(%a, %a, %s);"
63
    inject_copy_id
64
    pp_var var
65
    pp_var value
66
    (mpfr_rnd ())
67

    
68
let rec pp_inject_assign pp_var fmt var value =
69
  if is_const_value value
70
  then
71
    pp_inject_real pp_var pp_var fmt var value
72
  else
73
    pp_inject_copy pp_var fmt var value
74

    
75
let pp_inject_init pp_var fmt var =
76
  Format.fprintf fmt "%s(%a, %i);"
77
    inject_init_id
78
    pp_var var
79
    (mpfr_prec ())
80

    
81
let pp_inject_clear pp_var fmt var =
82
  Format.fprintf fmt "%s(%a);"
83
    inject_clear_id
84
    pp_var var
85

    
86
let base_inject_op id =
87
  match id with
88
  | "+"      -> "MPFRPlus"
89
  | "-"      -> "MPFRMinus"
90
  | "*"      -> "MPFRTimes"
91
  | "/"      -> "MPFRDiv"
92
  | "uminus" -> "MPFRUminus"
93
  | "<="     -> "MPFRLe"
94
  | "<"      -> "MPFRLt"
95
  | ">="     -> "MPFRGe"
96
  | ">"      -> "MPFRGt"
97
  | "="      -> "MPFREq"
98
  | "!="     -> "MPFRNeq"
99
  | _        -> raise Not_found
100

    
101
let inject_op id =
102
  try
103
    base_inject_op id
104
  with Not_found -> id
105

    
106
let homomorphic_funs =
107
  List.fold_right (fun id res -> try base_inject_op id :: res with Not_found -> res) Basic_library.internal_funs []
108

    
109
let is_homomorphic_fun id =
110
  List.mem id homomorphic_funs
111

    
112
let inject_call expr =
113
  match expr.expr_desc with
114
  | Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) ->
115
    { expr with expr_desc = Expr_appl (inject_op id, args, None) }
116
  | _ -> expr
117

    
118
let expr_of_const_array expr =
119
  match expr.expr_desc with
120
  | Expr_const (Const_array cl) ->
121
    let typ = Types.array_element_type expr.expr_type in
122
    let expr_of_const c =
123
      { expr_desc = Expr_const c;
124
	expr_type = typ;
125
	expr_clock = expr.expr_clock;
126
	expr_loc = expr.expr_loc;
127
	expr_delay = Delay.new_var ();
128
	expr_annot = None;
129
	expr_tag = new_tag ();
130
      }
131
    in { expr with expr_desc = Expr_array (List.map expr_of_const cl) }
132
  | _                           -> assert false
133

    
134
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
135
let rec inject_list alias node inject_element defvars elist =
136
  List.fold_right
137
    (fun t (defvars, qlist) ->
138
      let defvars, norm_t = inject_element alias node defvars t in
139
      (defvars, norm_t :: qlist)
140
    ) elist (defvars, [])
141

    
142
let rec inject_expr ?(alias=true) node defvars expr =
143
let res=
144
  match expr.expr_desc with
145
  | Expr_const (Const_real _)  -> mk_expr_alias_opt alias node defvars expr
146
  | Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)
147
  | Expr_const (Const_struct _) -> assert false
148
  | Expr_ident _
149
  | Expr_const _  -> defvars, expr
150
  | Expr_array elist ->
151
    let defvars, norm_elist = inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist in
152
    let norm_expr = { expr with expr_desc = Expr_array norm_elist } in
153
    defvars, norm_expr
154
  | Expr_power (e1, d) ->
155
    let defvars, norm_e1 = inject_expr node defvars e1 in
156
    let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in
157
    defvars, norm_expr
158
  | Expr_access (e1, d) ->
159
    let defvars, norm_e1 = inject_expr node defvars e1 in
160
    let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in
161
    defvars, norm_expr
162
  | Expr_tuple elist -> 
163
    let defvars, norm_elist =
164
      inject_list alias node (fun alias -> inject_expr ~alias:alias) defvars elist in
165
    let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in
166
    defvars, norm_expr
167
  | Expr_appl (id, args, r) ->
168
    let defvars, norm_args = inject_expr node defvars args in
169
    let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in
170
    mk_expr_alias_opt alias node defvars (inject_call norm_expr)
171
  | Expr_arrow _ -> defvars, expr
172
  | Expr_pre e ->
173
    let defvars, norm_e = inject_expr node defvars e in
174
    let norm_expr = { expr with expr_desc = Expr_pre norm_e } in
175
    defvars, norm_expr
176
  | Expr_fby (e1, e2) ->
177
    let defvars, norm_e1 = inject_expr node defvars e1 in
178
    let defvars, norm_e2 = inject_expr node defvars e2 in
179
    let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in
180
    defvars, norm_expr
181
  | Expr_when (e, c, l) ->
182
    let defvars, norm_e = inject_expr node defvars e in
183
    let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in
184
    defvars, norm_expr
185
  | Expr_ite (c, t, e) ->
186
    let defvars, norm_c = inject_expr node defvars c in
187
    let defvars, norm_t = inject_expr node defvars t in
188
    let defvars, norm_e = inject_expr node defvars e in
189
    let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in
190
    defvars, norm_expr
191
  | Expr_merge (c, hl) ->
192
    let defvars, norm_hl = inject_branches node defvars hl in
193
    let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in
194
    defvars, norm_expr
195
in
196
(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr Printers.pp_expr (snd res);*)
197
res
198

    
199
and inject_branches node defvars hl =
200
 List.fold_right
201
   (fun (t, h) (defvars, norm_q) ->
202
     let (defvars, norm_h) = inject_expr node defvars h in
203
     defvars, (t, norm_h) :: norm_q
204
   )
205
   hl (defvars, [])
206

    
207

    
208
let rec inject_eq node defvars eq =
209
  let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in
210
  let norm_eq = { eq with eq_rhs = norm_rhs } in
211
  norm_eq::defs', vars'
212

    
213
(** normalize_node node returns a normalized node, 
214
    ie. 
215
    - updated locals
216
    - new equations
217
    - 
218
*)
219
let inject_node node = 
220
  cpt_fresh := 0;
221
  let inputs_outputs = node.node_inputs@node.node_outputs in
222
  let is_local v =
223
    List.for_all ((!=) v) inputs_outputs in
224
  let orig_vars = inputs_outputs@node.node_locals in
225
  let defs, vars =
226
    let eqs, auts = get_node_eqs node in
227
    if auts != [] then assert false; (* Automata should be expanded by now. *)
228
    List.fold_left (inject_eq node) ([], orig_vars) eqs in
229
  (* Normalize the asserts *)
230
  let vars, assert_defs, asserts = 
231
    List.fold_left (
232
    fun (vars, def_accu, assert_accu) assert_ ->
233
      let assert_expr = assert_.assert_expr in
234
      let (defs, vars'), expr = 
235
	inject_expr 
236
	  ~alias:false 
237
	  node 
238
	  ([], vars) (* defvar only contains vars *)
239
	  assert_expr
240
      in
241
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
242
    ) (vars, [], []) node.node_asserts in
243
  let new_locals = List.filter is_local vars in
244
  (* Compute traceability info: 
245
     - gather newly bound variables
246
     - compute the associated expression without aliases     
247
  *)
248
  (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
249
  let node =
250
  { node with 
251
    node_locals = new_locals; 
252
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
253
  }
254
  in ((*Printers.pp_node Format.err_formatter node;*) node)
255

    
256
let inject_decl decl =
257
  match decl.top_decl_desc with
258
  | Node nd ->
259
    {decl with top_decl_desc = Node (inject_node nd)}
260
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
261
  
262
let inject_prog decls = 
263
  List.map inject_decl decls
264

    
265

    
266
(* Local Variables: *)
267
(* compile-command:"make -C .." *)
268
(* End: *)