Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/plugins/mpfr/lustrec_mpfr.ml
17 17
open Machine_code_common
18 18

  
19 19
let report = Log.report ~plugin:"MPFR"
20
           
21
let mpfr_module = mktop (Open(false, "mpfr_lustre"))
20

  
21
let mpfr_module = mktop (Open (false, "mpfr_lustre"))
22

  
22 23
let cpt_fresh = ref 0
23
  
24

  
24 25
let mpfr_rnd () = "MPFR_RNDN"
25 26

  
26 27
let mpfr_prec () = !Options.mpfr_prec
......
41 42
  not (Types.is_real_type value.value_type && is_const_value value)
42 43

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

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

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

  
64 56
let pp_inject_copy pp_var fmt (var, value) =
65
  Format.fprintf fmt "%s(%a, %a, %s);"
66
    inject_copy_id
67
    pp_var var
68
    pp_var value
57
  Format.fprintf fmt "%s(%a, %a, %s);" inject_copy_id pp_var var pp_var value
69 58
    (mpfr_rnd ())
70 59

  
71
let pp_inject_assign pp_var fmt (_, value as vv) =
72
  if is_const_value value
73
  then
74
    pp_inject_real pp_var pp_var fmt vv
75
  else
76
    pp_inject_copy pp_var fmt vv
60
let pp_inject_assign pp_var fmt ((_, value) as vv) =
61
  if is_const_value value then pp_inject_real pp_var pp_var fmt vv
62
  else pp_inject_copy pp_var fmt vv
77 63

  
78 64
let pp_inject_init pp_var fmt var =
79
  Format.fprintf fmt "%s(%a, %i);"
80
    inject_init_id
81
    pp_var var
82
    (mpfr_prec ())
65
  Format.fprintf fmt "%s(%a, %i);" inject_init_id pp_var var (mpfr_prec ())
83 66

  
84 67
let pp_inject_clear pp_var fmt var =
85
  Format.fprintf fmt "%s(%a);"
86
    inject_clear_id
87
    pp_var var
68
  Format.fprintf fmt "%s(%a);" inject_clear_id pp_var var
88 69

  
89 70
let base_inject_op id =
90 71
  match id with
91
  | "+"      -> "MPFRPlus"
92
  | "-"      -> "MPFRMinus"
93
  | "*"      -> "MPFRTimes"
94
  | "/"      -> "MPFRDiv"
95
  | "uminus" -> "MPFRUminus"
96
  | "<="     -> "MPFRLe"
97
  | "<"      -> "MPFRLt"
98
  | ">="     -> "MPFRGe"
99
  | ">"      -> "MPFRGt"
100
  | "="      -> "MPFREq"
101
  | "!="     -> "MPFRNeq"
72
  | "+" ->
73
    "MPFRPlus"
74
  | "-" ->
75
    "MPFRMinus"
76
  | "*" ->
77
    "MPFRTimes"
78
  | "/" ->
79
    "MPFRDiv"
80
  | "uminus" ->
81
    "MPFRUminus"
82
  | "<=" ->
83
    "MPFRLe"
84
  | "<" ->
85
    "MPFRLt"
86
  | ">=" ->
87
    "MPFRGe"
88
  | ">" ->
89
    "MPFRGt"
90
  | "=" ->
91
    "MPFREq"
92
  | "!=" ->
93
    "MPFRNeq"
102 94
  (* Conv functions *)
103
  | "int_to_real" -> "MPFRint_to_real"
104
  | "real_to_int" -> "MPFRreal_to_int"
105
  | "_floor" -> "MPFRfloor"        
106
  | "_ceil" -> "MPFRceil"        
107
  | "_round" -> "MPFRround"        
108
  | "_Floor" -> "MPFRFloor"        
109
  | "_Ceiling" -> "MPFRCeiling"        
110
  | "_Round" -> "MPFRRound"        
111
       
95
  | "int_to_real" ->
96
    "MPFRint_to_real"
97
  | "real_to_int" ->
98
    "MPFRreal_to_int"
99
  | "_floor" ->
100
    "MPFRfloor"
101
  | "_ceil" ->
102
    "MPFRceil"
103
  | "_round" ->
104
    "MPFRround"
105
  | "_Floor" ->
106
    "MPFRFloor"
107
  | "_Ceiling" ->
108
    "MPFRCeiling"
109
  | "_Round" ->
110
    "MPFRRound"
112 111
  (* Math library functions *)
113
  | "acos" -> "MPFRacos"
114
  | "acosh" -> "MPFRacosh"
115
  | "asin" -> "MPFRasin"
116
  | "asinh" -> "MPFRasinh"
117
  | "atan" -> "MPFRatan"
118
  | "atan2" -> "MPFRatan2"
119
  | "atanh" -> "MPFRatanh"
120
  | "cbrt" -> "MPFRcbrt"
121
  | "cos" -> "MPFRcos"
122
  | "cosh" -> "MPFRcosh"
123
  | "ceil" -> "MPFRceil"
124
  | "erf" -> "MPFRerf"
125
  | "exp" -> "MPFRexp"
126
  | "fabs" -> "MPFRfabs"
127
  | "floor" -> "MPFRfloor"
128
  | "fmod" -> "MPFRfmod"
129
  | "log" -> "MPFRlog"
130
  | "log10" -> "MPFRlog10"
131
  | "pow" -> "MPFRpow"
132
  | "round" -> "MPFRround"
133
  | "sin" -> "MPFRsin"
134
  | "sinh" -> "MPFRsinh"
135
  | "sqrt" -> "MPFRsqrt"
136
  | "trunc" -> "MPFRtrunc"
137
  | "tan" -> "MPFRtan"
138
  | _        -> raise Not_found
112
  | "acos" ->
113
    "MPFRacos"
114
  | "acosh" ->
115
    "MPFRacosh"
116
  | "asin" ->
117
    "MPFRasin"
118
  | "asinh" ->
119
    "MPFRasinh"
120
  | "atan" ->
121
    "MPFRatan"
122
  | "atan2" ->
123
    "MPFRatan2"
124
  | "atanh" ->
125
    "MPFRatanh"
126
  | "cbrt" ->
127
    "MPFRcbrt"
128
  | "cos" ->
129
    "MPFRcos"
130
  | "cosh" ->
131
    "MPFRcosh"
132
  | "ceil" ->
133
    "MPFRceil"
134
  | "erf" ->
135
    "MPFRerf"
136
  | "exp" ->
137
    "MPFRexp"
138
  | "fabs" ->
139
    "MPFRfabs"
140
  | "floor" ->
141
    "MPFRfloor"
142
  | "fmod" ->
143
    "MPFRfmod"
144
  | "log" ->
145
    "MPFRlog"
146
  | "log10" ->
147
    "MPFRlog10"
148
  | "pow" ->
149
    "MPFRpow"
150
  | "round" ->
151
    "MPFRround"
152
  | "sin" ->
153
    "MPFRsin"
154
  | "sinh" ->
155
    "MPFRsinh"
156
  | "sqrt" ->
157
    "MPFRsqrt"
158
  | "trunc" ->
159
    "MPFRtrunc"
160
  | "tan" ->
161
    "MPFRtan"
162
  | _ ->
163
    raise Not_found
139 164

  
140 165
let inject_op id =
141
  report ~level:3 (fun fmt -> Format.fprintf fmt "trying to inject mpfr into function %s@." id);
142
  try
143
    base_inject_op id
144
  with Not_found -> id
166
  report ~level:3 (fun fmt ->
167
      Format.fprintf fmt "trying to inject mpfr into function %s@." id);
168
  try base_inject_op id with Not_found -> id
145 169

  
146 170
let homomorphic_funs =
147
  List.fold_right (fun id res -> try base_inject_op id :: res with Not_found -> res) Basic_library.internal_funs []
171
  List.fold_right
172
    (fun id res -> try base_inject_op id :: res with Not_found -> res)
173
    Basic_library.internal_funs []
148 174

  
149
let is_homomorphic_fun id =
150
  List.mem id homomorphic_funs
175
let is_homomorphic_fun id = List.mem id homomorphic_funs
151 176

  
152 177
let inject_call expr =
153 178
  match expr.expr_desc with
154
  | Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) ->
179
  | Expr_appl (id, args, None)
180
    when not (Basic_library.is_expr_internal_fun expr) ->
155 181
    { expr with expr_desc = Expr_appl (inject_op id, args, None) }
156
  | _ -> expr
182
  | _ ->
183
    expr
157 184

  
158 185
let expr_of_const_array expr =
159 186
  match expr.expr_desc with
160 187
  | Expr_const (Const_array cl) ->
161 188
    let typ = Types.array_element_type expr.expr_type in
162 189
    let expr_of_const c =
163
      { expr_desc = Expr_const c;
164
	expr_type = typ;
165
	expr_clock = expr.expr_clock;
166
	expr_loc = expr.expr_loc;
167
	expr_delay = Delay.new_var ();
168
	expr_annot = None;
169
	expr_tag = new_tag ();
190
      {
191
        expr_desc = Expr_const c;
192
        expr_type = typ;
193
        expr_clock = expr.expr_clock;
194
        expr_loc = expr.expr_loc;
195
        expr_delay = Delay.new_var ();
196
        expr_annot = None;
197
        expr_tag = new_tag ();
170 198
      }
171
    in { expr with expr_desc = Expr_array (List.map expr_of_const cl) }
172
  | _                           -> assert false
199
    in
200
    { expr with expr_desc = Expr_array (List.map expr_of_const cl) }
201
  | _ ->
202
    assert false
173 203

  
174
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
204
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) *
205
   normalized <foo> *)
175 206
let inject_list alias node inject_element defvars elist =
176 207
  List.fold_right
177 208
    (fun t (defvars, qlist) ->
178 209
      let defvars, norm_t = inject_element alias node defvars t in
179
      (defvars, norm_t :: qlist)
180
    ) elist (defvars, [])
181

  
182
let rec inject_expr ?(alias=true) node defvars expr =
183
let res =
184
  match expr.expr_desc with
185
  | Expr_const (Const_real _)  -> mk_expr_alias_opt alias node defvars expr
186
  | Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)
187
  | Expr_const (Const_struct _) -> assert false
188
  | Expr_ident _
189
  | Expr_const _  -> defvars, expr
190
  | Expr_array elist ->
191
    let defvars, norm_elist = inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist in
192
    let norm_expr = { expr with expr_desc = Expr_array norm_elist } in
193
    defvars, norm_expr
194
  | Expr_power (e1, d) ->
195
    let defvars, norm_e1 = inject_expr node defvars e1 in
196
    let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in
197
    defvars, norm_expr
198
  | Expr_access (e1, d) ->
199
    let defvars, norm_e1 = inject_expr node defvars e1 in
200
    let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in
201
    defvars, norm_expr
202
  | Expr_tuple elist -> 
203
    let defvars, norm_elist =
204
      inject_list alias node (fun alias -> inject_expr ~alias:alias) defvars elist in
205
    let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in
206
    defvars, norm_expr
207
  | Expr_appl (id, args, r) ->
208
    let defvars, norm_args = inject_expr node defvars args in
209
    let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in
210
    mk_expr_alias_opt alias node defvars (inject_call norm_expr)
211
  | Expr_arrow _ -> defvars, expr
212
  | Expr_pre e ->
213
    let defvars, norm_e = inject_expr node defvars e in
214
    let norm_expr = { expr with expr_desc = Expr_pre norm_e } in
215
    defvars, norm_expr
216
  | Expr_fby (e1, e2) ->
217
    let defvars, norm_e1 = inject_expr node defvars e1 in
218
    let defvars, norm_e2 = inject_expr node defvars e2 in
219
    let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in
220
    defvars, norm_expr
221
  | Expr_when (e, c, l) ->
222
    let defvars, norm_e = inject_expr node defvars e in
223
    let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in
224
    defvars, norm_expr
225
  | Expr_ite (c, t, e) ->
226
    let defvars, norm_c = inject_expr node defvars c in
227
    let defvars, norm_t = inject_expr node defvars t in
228
    let defvars, norm_e = inject_expr node defvars e in
229
    let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in
230
    defvars, norm_expr
231
  | Expr_merge (c, hl) ->
232
    let defvars, norm_hl = inject_branches node defvars hl in
233
    let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in
234
    defvars, norm_expr
235
in
236
(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr Printers.pp_expr (snd res);*)
237
res
210
      defvars, norm_t :: qlist)
211
    elist (defvars, [])
212

  
213
let rec inject_expr ?(alias = true) node defvars expr =
214
  let res =
215
    match expr.expr_desc with
216
    | Expr_const (Const_real _) ->
217
      mk_expr_alias_opt alias node defvars expr
218
    | Expr_const (Const_array _) ->
219
      inject_expr ~alias node defvars (expr_of_const_array expr)
220
    | Expr_const (Const_struct _) ->
221
      assert false
222
    | Expr_ident _ | Expr_const _ ->
223
      defvars, expr
224
    | Expr_array elist ->
225
      let defvars, norm_elist =
226
        inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist
227
      in
228
      let norm_expr = { expr with expr_desc = Expr_array norm_elist } in
229
      defvars, norm_expr
230
    | Expr_power (e1, d) ->
231
      let defvars, norm_e1 = inject_expr node defvars e1 in
232
      let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in
233
      defvars, norm_expr
234
    | Expr_access (e1, d) ->
235
      let defvars, norm_e1 = inject_expr node defvars e1 in
236
      let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in
237
      defvars, norm_expr
238
    | Expr_tuple elist ->
239
      let defvars, norm_elist =
240
        inject_list alias node (fun alias -> inject_expr ~alias) defvars elist
241
      in
242
      let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in
243
      defvars, norm_expr
244
    | Expr_appl (id, args, r) ->
245
      let defvars, norm_args = inject_expr node defvars args in
246
      let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in
247
      mk_expr_alias_opt alias node defvars (inject_call norm_expr)
248
    | Expr_arrow _ ->
249
      defvars, expr
250
    | Expr_pre e ->
251
      let defvars, norm_e = inject_expr node defvars e in
252
      let norm_expr = { expr with expr_desc = Expr_pre norm_e } in
253
      defvars, norm_expr
254
    | Expr_fby (e1, e2) ->
255
      let defvars, norm_e1 = inject_expr node defvars e1 in
256
      let defvars, norm_e2 = inject_expr node defvars e2 in
257
      let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in
258
      defvars, norm_expr
259
    | Expr_when (e, c, l) ->
260
      let defvars, norm_e = inject_expr node defvars e in
261
      let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in
262
      defvars, norm_expr
263
    | Expr_ite (c, t, e) ->
264
      let defvars, norm_c = inject_expr node defvars c in
265
      let defvars, norm_t = inject_expr node defvars t in
266
      let defvars, norm_e = inject_expr node defvars e in
267
      let norm_expr =
268
        { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) }
269
      in
270
      defvars, norm_expr
271
    | Expr_merge (c, hl) ->
272
      let defvars, norm_hl = inject_branches node defvars hl in
273
      let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in
274
      defvars, norm_expr
275
  in
276
  (*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr
277
    Printers.pp_expr (snd res);*)
278
  res
238 279

  
239 280
and inject_branches node defvars hl =
240
 List.fold_right
241
   (fun (t, h) (defvars, norm_q) ->
242
     let (defvars, norm_h) = inject_expr node defvars h in
243
     defvars, (t, norm_h) :: norm_q
244
   )
245
   hl (defvars, [])
246

  
281
  List.fold_right
282
    (fun (t, h) (defvars, norm_q) ->
283
      let defvars, norm_h = inject_expr node defvars h in
284
      defvars, (t, norm_h) :: norm_q)
285
    hl (defvars, [])
247 286

  
248 287
let inject_eq node defvars eq =
249
  let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in
288
  let (defs', vars'), norm_rhs =
289
    inject_expr ~alias:false node defvars eq.eq_rhs
290
  in
250 291
  let norm_eq = { eq with eq_rhs = norm_rhs } in
251
  norm_eq::defs', vars'
292
  norm_eq :: defs', vars'
252 293

  
253 294
(* let inject_eexpr ee =
254 295
 *   { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr }
......
264 305
 *                 }
265 306
 *               ) s.modes
266 307
 *   } *)
267
  
268
(** normalize_node node returns a normalized node, 
269
    ie. 
270
    - updated locals
271
    - new equations
272
    - 
273
*)
274
let inject_node node = 
308

  
309
(** normalize_node node returns a normalized node, ie. - updated locals - new
310
    equations - *)
311
let inject_node node =
275 312
  cpt_fresh := 0;
276
  let inputs_outputs = node.node_inputs@node.node_outputs in
277
  let norm_ctx = (node.node_id, get_node_vars node) in
278
  let is_local v =
279
    List.for_all ((!=) v) inputs_outputs in
280
  let orig_vars = inputs_outputs@node.node_locals in
313
  let inputs_outputs = node.node_inputs @ node.node_outputs in
314
  let norm_ctx = node.node_id, get_node_vars node in
315
  let is_local v = List.for_all (( != ) v) inputs_outputs in
316
  let orig_vars = inputs_outputs @ node.node_locals in
281 317
  let defs, vars =
282 318
    let eqs, auts = get_node_eqs node in
283
    if auts != [] then assert false; (* Automata should be expanded by now. *)
284
    List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs in
319
    if auts != [] then assert false;
320
    (* Automata should be expanded by now. *)
321
    List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs
322
  in
285 323
  (* Normalize the asserts *)
286 324
  let vars, assert_defs, _ =
287
    List.fold_left (
288
    fun (vars, def_accu, assert_accu) assert_ ->
289
      let assert_expr = assert_.assert_expr in
290
      let (defs, vars'), expr = 
291
	inject_expr 
292
	  ~alias:false 
293
	  norm_ctx 
294
	  ([], vars) (* defvar only contains vars *)
295
	  assert_expr
296
      in
297
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
298
    ) (vars, [], []) node.node_asserts in
325
    List.fold_left
326
      (fun (vars, def_accu, assert_accu) assert_ ->
327
        let assert_expr = assert_.assert_expr in
328
        let (defs, vars'), expr =
329
          inject_expr ~alias:false norm_ctx ([], vars)
330
            (* defvar only contains vars *)
331
            assert_expr
332
        in
333
        ( vars',
334
          defs @ def_accu,
335
          { assert_ with assert_expr = expr } :: assert_accu ))
336
      (vars, [], []) node.node_asserts
337
  in
299 338
  let new_locals = List.filter is_local vars in
300
  (* Compute traceability info: 
301
     - gather newly bound variables
302
     - compute the associated expression without aliases     
303
  *)
304
  (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
339
  (* Compute traceability info: - gather newly bound variables - compute the
340
     associated expression without aliases *)
341
  (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals))
342
     new_locals in *)
305 343
  (* See comment below
306 344
   *  let spec = match node.node_spec with
307 345
   *   | None -> None
308 346
   *   | Some spec -> Some (inject_spec spec)
309 347
   * in *)
310 348
  let node =
311
  { node with 
312
    node_locals = new_locals; 
313
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
314
    (* Incomplete work: TODO. Do we have to inject MPFR code here?
315
       Does it make sense for annotations? For me, only if we produce
316
       C code for annotations. Otherwise the various verification
317
       backend should have their own understanding, but would not
318
       necessarily require this additional normalization. *)
319
    (* 
320
       node_spec = spec;
321
       node_annot = List.map (fun ann -> {ann with
322
           annots = List.map (fun (ids, ee) -> ids, inject_eexpr ee) ann.annots}
323
         ) node.node_annot *)
324
  }
325
  in ((*Printers.pp_node Format.err_formatter node;*) node)
349
    {
350
      node with
351
      node_locals = new_locals;
352
      node_stmts =
353
        List.map (fun eq -> Eq eq) (defs @ assert_defs)
354
        (* Incomplete work: TODO. Do we have to inject MPFR code here? Does it
355
           make sense for annotations? For me, only if we produce C code for
356
           annotations. Otherwise the various verification backend should have
357
           their own understanding, but would not necessarily require this
358
           additional normalization. *)
359
        (* node_spec = spec; node_annot = List.map (fun ann -> {ann with annots
360
           = List.map (fun (ids, ee) -> ids, inject_eexpr ee) ann.annots} )
361
           node.node_annot *);
362
    }
363
  in
364
  (*Printers.pp_node Format.err_formatter node;*)
365
  node
326 366

  
327 367
let inject_decl decl =
328 368
  match decl.top_decl_desc with
329 369
  | Node nd ->
330
    {decl with top_decl_desc = Node (inject_node nd)}
331
  | Include _ | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
332
  
333
let inject_prog decls = 
334
  List.map inject_decl decls
370
    { decl with top_decl_desc = Node (inject_node nd) }
371
  | Include _ | Open _ | ImportedNode _ | Const _ | TypeDef _ ->
372
    decl
335 373

  
374
let inject_prog decls = List.map inject_decl decls
336 375

  
337 376
(* Local Variables: *)
338 377
(* compile-command:"make -C .." *)

Also available in: Unified diff