Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / plugins / salsa / salsaDatatypes.ml @ 9a9058f4

History | View | Annotate | Download (13.3 KB)

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