Project

General

Profile

Download (13.3 KB) Statistics
| Branch: | Tag: | Revision:
1 8446bf03 ploc
module LT = Lustre_types
2
module MT = Machine_code_types
3 2863281f ploc
module MC = Machine_code_common
4 94c457b7 ploc
module ST = Salsa.Types
5 53206908 xthirioux
6 94c457b7 ploc
let debug = ref false
7 53206908 xthirioux
8 ca7ff3f7 Lélio Brun
let _ = Salsa.Prelude.sliceSize := 5
9
10
let pp_hash ~sep f fmt r =
11 53206908 xthirioux
  Format.fprintf fmt "[@[<v>";
12
  Hashtbl.iter (fun k v -> Format.fprintf fmt "%t%s@ " (f k v) sep) r;
13 ca7ff3f7 Lélio Brun
  Format.fprintf fmt "]@]"
14 53206908 xthirioux
15 ca7ff3f7 Lélio Brun
module type VALUE = sig
16 8e6cab20 ploc
  type t
17 53206908 xthirioux
18 ca7ff3f7 Lélio Brun
  val union : t -> t -> t
19 68322df3 ploc
20 ca7ff3f7 Lélio Brun
  val pp : Format.formatter -> t -> unit
21
22
  val leq : t -> t -> bool
23 53206908 xthirioux
end
24
25 ca7ff3f7 Lélio Brun
module Ranges =
26
functor
27
  (Value : VALUE)
28
  ->
29
  struct
30
    module Value = Value
31 53206908 xthirioux
32 ca7ff3f7 Lélio Brun
    type t = Value.t
33 8e6cab20 ploc
34 ca7ff3f7 Lélio Brun
    type r_t = (LT.ident, Value.t) Hashtbl.t
35 53206908 xthirioux
36 ca7ff3f7 Lélio Brun
    let empty : r_t = Hashtbl.create 13
37 53206908 xthirioux
38 ca7ff3f7 Lélio Brun
    (* Look for def of node i with inputs living in vtl_ranges, reinforce ranges
39
       to bound vdl: each output of node i *)
40
    let add_call ranges vdl id vtl_ranges = ranges
41
    (* TODO assert false. On est pas obligé de faire qqchose. On peut supposer
42
       que les ranges sont donnés pour chaque noeud *)
43 53206908 xthirioux
44 ca7ff3f7 Lélio Brun
    let pp fmt r =
45
      if Hashtbl.length r = 0 then Format.fprintf fmt "empty"
46
      else
47
        pp_hash ~sep:";"
48
          (fun k v fmt -> Format.fprintf fmt "%s -> %a" k Value.pp v)
49
          fmt r
50
51
    let pp_val = Value.pp
52
53
    let add_def ranges name r =
54
      (* Format.eprintf "%s: declare %a@."  *)
55
      (* 	  x.LT.var_id *)
56
      (* 	  Value.pp r ; *)
57
      let fresh = Hashtbl.copy ranges in
58
      Hashtbl.add fresh name r;
59
      fresh
60
61
    let enlarge ranges name r =
62
      let fresh = Hashtbl.copy ranges in
63
      if Hashtbl.mem fresh name then
64
        Hashtbl.replace fresh name (Value.union r (Hashtbl.find fresh name))
65
      else Hashtbl.add fresh name r;
66
      fresh
67
68
    (* Compute a join per variable *)
69
    let merge ranges1 ranges2 =
70
      (* Format.eprintf "Mergeing rangesint %a with %a@." pp ranges1 pp ranges2; *)
71
      let ranges = Hashtbl.copy ranges1 in
72
      Hashtbl.iter
73
        (fun k v ->
74
          if Hashtbl.mem ranges k then
75
            (* Format.eprintf "%s: %a union %a = %a@."  *)
76
            (*   k *)
77
            (*   Value.pp v  *)
78
            (*   Value.pp (Hashtbl.find ranges k) *)
79
            (*   Value.pp (Value.union v (Hashtbl.find ranges k)); *)
80
            Hashtbl.replace ranges k (Value.union v (Hashtbl.find ranges k))
81
          else Hashtbl.add ranges k v)
82
        ranges2;
83
      (* Format.eprintf "Merge result %a@." pp ranges; *)
84
      ranges
85 53206908 xthirioux
86 ca7ff3f7 Lélio Brun
    let to_abstract_env ranges =
87
      Hashtbl.fold (fun id value accu -> (id, value) :: accu) ranges []
88
  end
89 53206908 xthirioux
90 ca7ff3f7 Lélio Brun
module FloatIntSalsa = struct
91
  type t = ST.abstractValue
92 53206908 xthirioux
93 ca7ff3f7 Lélio Brun
  let pp fmt ((f, r) : t) =
94
    let fs, rs = Salsa.Float.Domain.print (f, r) in
95
    Format.fprintf fmt "%s + %s" fs rs
96 53206908 xthirioux
97 ca7ff3f7 Lélio Brun
  (* match f, r with | ST.I(a,b), ST.J(c,d) -> Format.fprintf fmt "[%f, %f] +
98
     [%s, %s]" a b (Num.string_of_num c) (Num.string_of_num d) | ST.I(a,b),
99
     ST.JInfty -> Format.fprintf fmt "[%f, %f] + oo" a b | ST.Empty, _ ->
100
     Format.fprintf fmt "???"
101 53206908 xthirioux
102 ca7ff3f7 Lélio Brun
     | _ -> assert false *)
103
  let union v1 v2 = Salsa.Float.Domain.join v1 v2
104 53206908 xthirioux
105 ca7ff3f7 Lélio Brun
  (* match v1, v2 with |(ST.I(x1, x2), ST.J(y1, y2)), (ST.I(x1', x2'), ST.J(y1',
106
     y2')) -> ST.(I(min x1 x1', max x2 x2'), J(min y1 y1', max y2 y2')) | _ ->
107
     Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false *)
108
  let inject cst =
109
    match cst with
110
    | LT.Const_int i ->
111
      Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_int i)
112
    | LT.Const_real r ->
113
      (* TODO: this is incorrect. We should rather compute the error associated
114
         to the float *)
115
      (* let f = float_of_string s in *)
116
      let n = Real.to_q r in
117
      Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_q n)
118
    (* let r = Salsa.Prelude.r_of_f_aux r in *)
119
    (* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *)
120
121
    (* let r = float_of_string s  in *)
122
    (* if r = 0. then *)
123
    (* Salsa.Builder.mk_cst (ST.R(-. min_float, min_float),Float.ulp (ST.R(-.
124
       min_float, min_float))) *)
125
    (* else *)
126
    (* Salsa.Builder.mk_cst
127
       (ST.I(r*.(1.-.epsilon_float),r*.(1.+.epsilon_float)),Float.ulp
128
       (ST.I(r,r))) *)
129
    | _ ->
130
      assert false
131
132
  let leq =
133
    (* Salsa.Float.feSseq *)
134
    Salsa.Float.Domain.leq
135
end
136 53206908 xthirioux
137 ca7ff3f7 Lélio Brun
module RangesInt = Ranges (FloatIntSalsa)
138 53206908 xthirioux
139 ca7ff3f7 Lélio Brun
module Vars = struct
140
  module VarSet = Set.Make (struct
141
    type t = LT.var_decl
142 53206908 xthirioux
143 ca7ff3f7 Lélio Brun
    let compare x y = compare x.LT.var_id y.LT.var_id
144
  end)
145 53206908 xthirioux
146 ca7ff3f7 Lélio Brun
  let real_vars vs =
147
    VarSet.filter (fun v -> Types.is_real_type v.LT.var_type) vs
148
149
  let of_list = List.fold_left (fun s e -> VarSet.add e s) VarSet.empty
150
151
  include VarSet
152
153
  let remove_list (set : t) (v_list : elt list) : t =
154
    List.fold_right VarSet.remove v_list set
155
156
  let pp fmt vs =
157
    Utils.fprintf_list ~sep:", " Printers.pp_var fmt (VarSet.elements vs)
158
end
159 53206908 xthirioux
160
(*************************************************************************************)
161 ca7ff3f7 Lélio Brun
(* Converting values back and forth *)
162 53206908 xthirioux
(*************************************************************************************)
163
164 ca7ff3f7 Lélio Brun
let rec value_t2salsa_expr constEnv vt =
165 53206908 xthirioux
  let value_t2salsa_expr = value_t2salsa_expr constEnv in
166 ca7ff3f7 Lélio Brun
  let res =
167 8446bf03 ploc
    match vt.MT.value_desc with
168 53206908 xthirioux
    (* | LT.Cst(LT.Const_tag(t) as c)   ->  *)
169
    (*   Format.eprintf "v2s: cst tag@."; *)
170
    (*   if List.mem_assoc t constEnv then ( *)
171
    (* 	Format.eprintf "trouvé la constante %s: %a@ " t Printers.pp_const c; *)
172
    (* 	FloatIntSalsa.inject (List.assoc t constEnv) *)
173
    (*   ) *)
174
    (*   else (     *)
175
    (* 	Format.eprintf "Const tag %s unhandled@.@?" t ; *)
176 ca7ff3f7 Lélio Brun
    (* raise (Salsa.Prelude.Error ("Entschuldigung6, constant tag not yet
177
       implemented")) *)
178
    (* ) *)
179
    | MT.Cst cst ->
180
      (* Format.eprintf "v2s: cst tag 2: %a@." Printers.pp_const cst; *)
181
      FloatIntSalsa.inject cst
182
    | MT.Var v ->
183
      (* Format.eprintf "v2s: var %s@." v.LT.var_id; *)
184
      let sel_fun (vname, _) = v.LT.var_id = vname in
185
      if List.exists sel_fun constEnv then
186
        let _, cst = List.find sel_fun constEnv in
187
        FloatIntSalsa.inject cst
188 53206908 xthirioux
      else
189 ca7ff3f7 Lélio Brun
        let id = v.LT.var_id in
190
        Salsa.Builder.mk_id id
191
    | MT.Fun (binop, [ x; y ]) ->
192
      let salsaX = value_t2salsa_expr x in
193
      let salsaY = value_t2salsa_expr y in
194
      let op =
195
        let pred f x y = Salsa.Builder.mk_int_of_bool (f x y) in
196
        match binop with
197
        | "+" ->
198
          Salsa.Builder.mk_plus
199
        | "-" ->
200
          Salsa.Builder.mk_minus
201
        | "*" ->
202
          Salsa.Builder.mk_times
203
        | "/" ->
204
          Salsa.Builder.mk_div
205
        | "=" ->
206
          pred Salsa.Builder.mk_eq
207
        | "<" ->
208
          pred Salsa.Builder.mk_lt
209
        | ">" ->
210
          pred Salsa.Builder.mk_gt
211
        | "<=" ->
212
          pred Salsa.Builder.mk_lte
213
        | ">=" ->
214
          pred Salsa.Builder.mk_gte
215
        | _ ->
216
          assert false
217
      in
218
      op salsaX salsaY
219
    | MT.Fun (unop, [ x ]) ->
220
      let salsaX = value_t2salsa_expr x in
221
      Salsa.Builder.mk_uminus salsaX
222
    | MT.Fun (f, _) ->
223
      raise
224
        (Salsa.Prelude.Error
225
           ("Unhandled function " ^ f ^ " in conversion to salsa expression"))
226
    | MT.Array _ | MT.Access _ | MT.Power _ ->
227
      raise
228
        (Salsa.Prelude.Error
229
           "Unhandled construct in conversion to salsa expression")
230 53206908 xthirioux
  in
231
  (* if debug then *)
232
  (*   Format.eprintf "value_t2salsa_expr: %a -> %a@ " *)
233
  (*     MC.pp_val vt *)
234 ca7ff3f7 Lélio Brun
  (* (fun fmt x -> Format.fprintf fmt "%s" (Salsa.Print.printExpression x)) res; *)
235 53206908 xthirioux
  res
236
237 ca7ff3f7 Lélio Brun
type var_decl = { vdecl : LT.var_decl; is_local : bool }
238
239
module VarEnv = Map.Make (struct
240
  type t = LT.ident
241
242
  let compare = compare
243
end)
244 53206908 xthirioux
245
(* let is_local_var vars_env v = *)
246
(*   try *)
247
(*   (VarEnv.find v vars_env).is_local *)
248 ca7ff3f7 Lélio Brun
(* with Not_found -> Format.eprintf "Impossible to find var %s@.@?" v; assert
249
   false *)
250 53206908 xthirioux
251
let get_var vars_env v =
252 ca7ff3f7 Lélio Brun
  try VarEnv.find v vars_env
253
  with Not_found ->
254
    Format.eprintf "Impossible to find var %s in var env %a@ " v
255
      (Utils.fprintf_list ~sep:", " (fun fmt (id, _) ->
256
           Format.pp_print_string fmt id))
257
      (VarEnv.bindings vars_env);
258
    assert false
259 53206908 xthirioux
260
let compute_vars_env m =
261
  let env = VarEnv.empty in
262 ca7ff3f7 Lélio Brun
  let env =
263
    List.fold_left
264
      (fun accu v ->
265
        VarEnv.add v.LT.var_id { vdecl = v; is_local = false } accu)
266
      env m.MT.mmemory
267 53206908 xthirioux
  in
268 ca7ff3f7 Lélio Brun
  let env =
269
    List.fold_left
270
      (fun accu v -> VarEnv.add v.LT.var_id { vdecl = v; is_local = true } accu)
271 53206908 xthirioux
      env
272 ca7ff3f7 Lélio Brun
      MC.(
273
        m.MT.mstep.MT.step_inputs @ m.MT.mstep.MT.step_outputs
274
        @ m.MT.mstep.MT.step_locals)
275 53206908 xthirioux
  in
276 ca7ff3f7 Lélio Brun
  env
277 53206908 xthirioux
278 ca7ff3f7 Lélio Brun
let rec salsa_expr2value_t vars_env cst_env e =
279
  (* let e = Float.evalPartExpr e [] [] in *)
280 53206908 xthirioux
  let salsa_expr2value_t = salsa_expr2value_t vars_env cst_env in
281 ca7ff3f7 Lélio Brun
  let binop op e1 e2 t =
282 53206908 xthirioux
    let x = salsa_expr2value_t e1 in
283 ca7ff3f7 Lélio Brun
    let y = salsa_expr2value_t e2 in
284
    MC.mk_val (MT.Fun (op, [ x; y ])) t
285 53206908 xthirioux
  in
286
  match e with
287 ca7ff3f7 Lélio Brun
  | ST.Cst (abs_val, _) ->
288
    (* We project ranges into constants. We forget about errors and provide the
289
       mean/middle value of the interval *)
290 151117f7 ploc
    let new_float = Salsa.Float.Domain.to_float abs_val in
291 ca7ff3f7 Lélio Brun
    (* let  new_float = Salsa.NumMartel.float_of_num c in *)
292
    (* let new_float =  *)
293
    (* 	if f1 = f2 then *)
294
    (* 	  f1 *)
295
    (* 	else *)
296
    (* 	  (f1 +. f2) /. 2.0  *)
297
    (* in *)
298
    (* Log.report ~level:3 *)
299
    (* (fun fmt -> Format.fprintf fmt "projecting [%.45f, %.45f] -> %.45f@ " f1
300
       f2 new_float); *)
301
    let cst =
302
      let s =
303
        if new_float = 0. then "0."
304
        else
305
          (* We have to convert it into our format: int * int * real *)
306
          (* string_of_float new_float *)
307
          let _ = Format.flush_str_formatter () in
308
          Format.fprintf Format.str_formatter "%.11f" new_float;
309
          Format.flush_str_formatter ()
310 53206908 xthirioux
      in
311 ca7ff3f7 Lélio Brun
      Parser_lustre.signed_const Lexer_lustre.token (Lexing.from_string s)
312
    in
313
    MC.mk_val (MT.Cst cst) Type_predef.type_real
314
  | ST.Id (id, _) ->
315 9b8acef5 ploc
    (* Format.eprintf "Looking for id=%s@.@?" id; *)
316 ca7ff3f7 Lélio Brun
    if List.mem_assoc id cst_env then
317
      let cst = List.assoc id cst_env in
318 9b8acef5 ploc
      (* Format.eprintf "Found cst = %a@.@?" Printers.pp_const cst; *)
319 ca7ff3f7 Lélio Brun
      MC.mk_val (MT.Cst cst) Type_predef.type_real
320
    else
321 53206908 xthirioux
      (* if is_const salsa_label then *)
322
      (*   MC.Cst(LT.Const_tag(get_const salsa_label)) *)
323 ca7ff3f7 Lélio Brun
      (* else *)
324
      let var_id = try get_var vars_env id with Not_found -> assert false in
325
      MC.mk_val (MT.Var var_id.vdecl) var_id.vdecl.LT.var_type
326
  | ST.Plus (x, y, _) ->
327
    binop "+" x y Type_predef.type_real
328
  | ST.Minus (x, y, _) ->
329
    binop "-" x y Type_predef.type_real
330
  | ST.Times (x, y, _) ->
331
    binop "*" x y Type_predef.type_real
332
  | ST.Div (x, y, _) ->
333
    binop "/" x y Type_predef.type_real
334
  | ST.Uminus (x, _) ->
335
    let x = salsa_expr2value_t x in
336
    MC.mk_val (MT.Fun ("uminus", [ x ])) Type_predef.type_real
337
  | ST.IntOfBool (ST.Eq (x, y, _), _) ->
338
    binop "=" x y Type_predef.type_bool
339
  | ST.IntOfBool (ST.Lt (x, y, _), _) ->
340
    binop "<" x y Type_predef.type_bool
341
  | ST.IntOfBool (ST.Gt (x, y, _), _) ->
342
    binop ">" x y Type_predef.type_bool
343
  | ST.IntOfBool (ST.Lte (x, y, _), _) ->
344
    binop "<=" x y Type_predef.type_bool
345
  | ST.IntOfBool (ST.Gte (x, y, _), _) ->
346
    binop ">=" x y Type_predef.type_bool
347
  | _ ->
348
    raise
349
      (Salsa.Prelude.Error
350
         "Entschuldigung, salsaExpr2value_t case not yet implemented")
351 9a3c3d8f Ploc
352 53206908 xthirioux
let rec get_salsa_free_vars vars_env constEnv absenv e =
353
  let f = get_salsa_free_vars vars_env constEnv absenv in
354
  match e with
355 ca7ff3f7 Lélio Brun
  | ST.Id (id, _) ->
356
    if (not (List.mem_assoc id absenv)) && not (List.mem_assoc id constEnv) then
357
      Vars.singleton
358
        (try VarEnv.find id vars_env with Not_found -> assert false).vdecl
359
    else Vars.empty
360
  | ST.Plus (x, y, _)
361
  | ST.Minus (x, y, _)
362
  | ST.Times (x, y, _)
363
  | ST.Div (x, y, _)
364
  | ST.IntOfBool (ST.Eq (x, y, _), _)
365
  | ST.IntOfBool (ST.Lt (x, y, _), _)
366
  | ST.IntOfBool (ST.Gt (x, y, _), _)
367
  | ST.IntOfBool (ST.Lte (x, y, _), _)
368
  | ST.IntOfBool (ST.Gte (x, y, _), _) ->
369
    Vars.union (f x) (f y)
370
  | ST.Uminus (x, _) ->
371
    f x
372
  | ST.Cst _ ->
373
    Vars.empty
374
  | _ ->
375
    assert false
376
377
module FormalEnv = struct
378
  type fe_t = (LT.ident, int * MT.value_t) Hashtbl.t
379
380 642e116d ploc
  let cpt = ref 0
381
382
  exception NoDefinition of LT.var_decl
383 ca7ff3f7 Lélio Brun
384 642e116d ploc
  (* Returns the expression associated to v in env *)
385 ca7ff3f7 Lélio Brun
  let get_def (env : fe_t) v =
386
    try snd (Hashtbl.find env v.LT.var_id)
387 642e116d ploc
    with Not_found -> raise (NoDefinition v)
388
389 ca7ff3f7 Lélio Brun
  let fold f = Hashtbl.fold (fun k (_, v) accu -> f k v accu)
390
391
  let to_salsa constEnv formalEnv =
392
    fold
393
      (fun id expr accu -> (id, value_t2salsa_expr constEnv expr) :: accu)
394
      formalEnv []
395 642e116d ploc
396 ca7ff3f7 Lélio Brun
  let def constEnv vars_env (env : fe_t) d expr =
397 642e116d ploc
    incr cpt;
398
    let fresh = Hashtbl.copy env in
399
    let expr_salsa = value_t2salsa_expr constEnv expr in
400
    let salsa_env = to_salsa constEnv env in
401
    let expr_salsa, _ = Salsa.Rewrite.substVars expr_salsa salsa_env 0 in
402 ca7ff3f7 Lélio Brun
    let expr_salsa =
403
      Salsa.Analyzer.evalPartExpr expr_salsa salsa_env []
404
        (* no blacklisted vars *)
405
        []
406
      (*no arrays *)
407
    in
408 642e116d ploc
    let expr_lustrec = salsa_expr2value_t vars_env [] expr_salsa in
409 ca7ff3f7 Lélio Brun
    Hashtbl.add fresh d.LT.var_id (!cpt, expr_lustrec);
410
    fresh
411 642e116d ploc
412 ca7ff3f7 Lélio Brun
  let empty () : fe_t = Hashtbl.create 13
413 642e116d ploc
414 ca7ff3f7 Lélio Brun
  let pp m fmt env =
415
    pp_hash ~sep:";@ "
416
      (fun k (_, v) fmt -> Format.fprintf fmt "%s -> %a" k (MC.pp_val m) v)
417
      fmt env
418 642e116d ploc
419
  let get_sort_fun env =
420 ca7ff3f7 Lélio Brun
    let order = Hashtbl.fold (fun k (cpt, _) accu -> (k, cpt) :: accu) env [] in
421
    fun v1 v2 ->
422
      if List.mem_assoc v1.LT.var_id order && List.mem_assoc v2.LT.var_id order
423
      then
424
        if List.assoc v1.LT.var_id order <= List.assoc v2.LT.var_id order then
425
          -1
426
        else 1
427
      else assert false
428 642e116d ploc
end
429
430 53206908 xthirioux
(* Local Variables: *)
431
(* compile-command:"make -C ../../.." *)
432
(* End: *)