Project

General

Profile

Revision 05ca2715 src/plugins/mpfr/mpfr.ml

View differences:

src/plugins/mpfr/mpfr.ml
10 10
(********************************************************************)
11 11

  
12 12
open Utils
13
open LustreSpec
13
open Lustre_types
14
open Machine_code_types
14 15
open Corelang
15 16
open Normalization
16
open Machine_code
17
open Machine_code_common
17 18

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

  
20
let cpt_fresh = ref 0
21
  
20 22
let mpfr_rnd () = "MPFR_RNDN"
21 23

  
22 24
let mpfr_prec () = !Options.mpfr_prec
......
43 45
    expr_clock = expr.expr_clock;
44 46
  }
45 47

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

  
53 55
let inject_assign expr =
......
67 69
let rec pp_inject_assign pp_var fmt var value =
68 70
  if is_const_value value
69 71
  then
70
    pp_inject_real pp_var fmt var value
72
    pp_inject_real pp_var pp_var fmt var value
71 73
  else
72 74
    pp_inject_copy pp_var fmt var value
73 75

  
......
139 141
    ) elist (defvars, [])
140 142

  
141 143
let rec inject_expr ?(alias=true) node defvars expr =
142
let res=
144
let res =
143 145
  match expr.expr_desc with
144 146
  | Expr_const (Const_real _)  -> mk_expr_alias_opt alias node defvars expr
145 147
  | Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)
......
209 211
  let norm_eq = { eq with eq_rhs = norm_rhs } in
210 212
  norm_eq::defs', vars'
211 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
  
212 229
(** normalize_node node returns a normalized node, 
213 230
    ie. 
214 231
    - updated locals
......
221 238
  let is_local v =
222 239
    List.for_all ((!=) v) inputs_outputs in
223 240
  let orig_vars = inputs_outputs@node.node_locals in
224
  let defs, vars = 
225
    List.fold_left (inject_eq node) ([], orig_vars) (get_node_eqs node) 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
226 245
  (* Normalize the asserts *)
227 246
  let vars, assert_defs, asserts = 
228 247
    List.fold_left (
......
243 262
     - compute the associated expression without aliases     
244 263
  *)
245 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 *)
246 270
  let node =
247 271
  { node with 
248 272
    node_locals = new_locals; 
249 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 *)
250 284
  }
251 285
  in ((*Printers.pp_node Format.err_formatter node;*) node)
252 286

  

Also available in: Unified diff