Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / mpfr.ml @ 0d54d8a8

History | View | Annotate | Download (9.71 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_common
18

    
19
let mpfr_module = mktop (Open(false, "mpfr_lustre"))
20
let cpt_fresh = ref 0
21
  
22
let mpfr_rnd () = "MPFR_RNDN"
23

    
24
let mpfr_prec () = !Options.mpfr_prec
25

    
26
let inject_id = "MPFRId"
27

    
28
let inject_copy_id = "mpfr_set"
29

    
30
let inject_real_id = "mpfr_set_flt"
31

    
32
let inject_init_id = "mpfr_init2"
33

    
34
let inject_clear_id = "mpfr_clear"
35

    
36
let mpfr_t = "mpfr_t"
37

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
208

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

    
214
(* let inject_eexpr ee =
215
 *   { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr }
216
 *   
217
 * let inject_spec s =
218
 *   { s with
219
 *     assume = List.map inject_eexpr s.assume;
220
 *     guarantees = List.map inject_eexpr s.guarantees;
221
 *     modes = List.map (fun m ->
222
 *                 { m with
223
 *                   require = List.map inject_eexpr m.require;
224
 *                   ensure = List.map inject_eexpr m.ensure
225
 *                 }
226
 *               ) s.modes
227
 *   } *)
228
  
229
(** normalize_node node returns a normalized node, 
230
    ie. 
231
    - updated locals
232
    - new equations
233
    - 
234
*)
235
let inject_node node = 
236
  cpt_fresh := 0;
237
  let inputs_outputs = node.node_inputs@node.node_outputs in
238
  let is_local v =
239
    List.for_all ((!=) v) inputs_outputs in
240
  let orig_vars = inputs_outputs@node.node_locals in
241
  let defs, vars =
242
    let eqs, auts = get_node_eqs node in
243
    if auts != [] then assert false; (* Automata should be expanded by now. *)
244
    List.fold_left (inject_eq node) ([], orig_vars) eqs in
245
  (* Normalize the asserts *)
246
  let vars, assert_defs, asserts = 
247
    List.fold_left (
248
    fun (vars, def_accu, assert_accu) assert_ ->
249
      let assert_expr = assert_.assert_expr in
250
      let (defs, vars'), expr = 
251
	inject_expr 
252
	  ~alias:false 
253
	  node 
254
	  ([], vars) (* defvar only contains vars *)
255
	  assert_expr
256
      in
257
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
258
    ) (vars, [], []) node.node_asserts in
259
  let new_locals = List.filter is_local vars in
260
  (* Compute traceability info: 
261
     - gather newly bound variables
262
     - compute the associated expression without aliases     
263
  *)
264
  (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
265
  (* See comment below
266
   *  let spec = match node.node_spec with
267
   *   | None -> None
268
   *   | Some spec -> Some (inject_spec spec)
269
   * in *)
270
  let node =
271
  { node with 
272
    node_locals = new_locals; 
273
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
274
    (* Incomplete work: TODO. Do we have to inject MPFR code here?
275
       Does it make sense for annotations? For me, only if we produce
276
       C code for annotations. Otherwise the various verification
277
       backend should have their own understanding, but would not
278
       necessarily require this additional normalization. *)
279
    (* 
280
       node_spec = spec;
281
       node_annot = List.map (fun ann -> {ann with
282
           annots = List.map (fun (ids, ee) -> ids, inject_eexpr ee) ann.annots}
283
         ) node.node_annot *)
284
  }
285
  in ((*Printers.pp_node Format.err_formatter node;*) node)
286

    
287
let inject_decl decl =
288
  match decl.top_decl_desc with
289
  | Node nd ->
290
    {decl with top_decl_desc = Node (inject_node nd)}
291
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
292
  
293
let inject_prog decls = 
294
  List.map inject_decl decls
295

    
296

    
297
(* Local Variables: *)
298
(* compile-command:"make -C .." *)
299
(* End: *)