Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / plugins / salsa / salsaDatatypes.ml @ 642e116d

History | View | Annotate | Download (12.5 KB)

1
module LT = LustreSpec
2
module MC = Machine_code
3
module ST = Salsa.Types
4
module Float = Salsa.Float
5

    
6
let debug = ref false
7

    
8
let pp_hash ~sep f fmt r = 
9
  Format.fprintf fmt "[@[<v>";
10
  Hashtbl.iter (fun k v -> Format.fprintf fmt "%t%s@ " (f k v) sep) r;
11
  Format.fprintf fmt "]@]";
12

    
13

    
14
module Ranges = 
15
  functor (Value: sig type t val union: t -> t -> t val pp: Format.formatter -> t -> unit end)  ->
16
struct
17
  type t = Value.t
18
  type r_t = (LT.ident, Value.t) Hashtbl.t
19

    
20
  let empty: r_t = Hashtbl.create 13
21

    
22
  (* Look for def of node i with inputs living in vtl_ranges, reinforce ranges
23
     to bound vdl: each output of node i *)
24
  let add_call ranges vdl id vtl_ranges = ranges (* TODO assert false.  On est
25
  						    pas obligé de faire
26
  						    qqchose. On peut supposer
27
  						    que les ranges sont donnés
28
  						    pour chaque noeud *)
29

    
30

    
31
  let pp = pp_hash ~sep:";" (fun k v fmt -> Format.fprintf fmt "%s -> %a" k Value.pp v) 
32
  let pp_val = Value.pp
33

    
34
  let add_def ranges name r = 
35
    (* Format.eprintf "%s: declare %a@."  *)
36
    (* 	  x.LT.var_id *)
37
    (* 	  Value.pp r ; *)
38
	
39
    let fresh = Hashtbl.copy ranges in
40
    Hashtbl.add fresh name r; fresh
41

    
42
  let enlarge ranges name r =
43
    let fresh = Hashtbl.copy ranges in
44
    if Hashtbl.mem fresh name then
45
      Hashtbl.replace fresh name (Value.union r (Hashtbl.find fresh name))
46
    else
47
      Hashtbl.add fresh name r; 
48
    fresh
49
    
50

    
51
  (* Compute a join per variable *)  
52
  let merge ranges1 ranges2 = 
53
    (* Format.eprintf "Mergeing rangesint %a with %a@." pp ranges1 pp ranges2; *)
54
    let ranges = Hashtbl.copy ranges1 in
55
    Hashtbl.iter (fun k v -> 
56
      if Hashtbl.mem ranges k then (
57
	(* Format.eprintf "%s: %a union %a = %a@."  *)
58
	(*   k *)
59
	(*   Value.pp v  *)
60
	(*   Value.pp (Hashtbl.find ranges k) *)
61
	(*   Value.pp (Value.union v (Hashtbl.find ranges k)); *)
62
      Hashtbl.replace ranges k (Value.union v (Hashtbl.find ranges k))
63
    )
64
      else
65
	 Hashtbl.add ranges k v
66
    ) ranges2;
67
    (* Format.eprintf "Merge result %a@." pp ranges; *)
68
    ranges
69

    
70
end
71

    
72
module FloatIntSalsa = 
73
struct
74
  type t = ST.abstractValue
75

    
76
  let pp fmt (f,r) =
77
    let fs, rs = (Salsa.Float.Domain.print (f,r)) in
78
    Format.fprintf fmt "%s + %s" fs rs 
79
(*    match f, r with
80
    | ST.I(a,b), ST.J(c,d) ->
81
      Format.fprintf fmt "[%f, %f] + [%s, %s]" a b (Num.string_of_num c) (Num.string_of_num d)
82
    | ST.I(a,b), ST.JInfty ->  Format.fprintf fmt "[%f, %f] + oo" a b 
83
    | ST.Empty, _ -> Format.fprintf fmt "???"
84

    
85
    | _ -> assert false
86
*)
87
  let union v1 v2 = Salsa.Float.Domain.join v1 v2
88
(*    match v1, v2 with
89
    |(ST.I(x1, x2), ST.J(y1, y2)), (ST.I(x1', x2'), ST.J(y1', y2')) ->
90
      ST.(I(min x1 x1', max x2 x2'), J(min y1 y1', max y2 y2'))
91
    | _ -> Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false 
92
*)
93
  let inject cst = match cst with (* ATTENTION ATTENTION !!!!! Remettre les Num !!!! *) 
94
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (ST.R(float_of_int i (*Num.num_of_int i*), []), ST.R(float_of_int i (*Num.num_of_int i*), []))
95
    | LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather
96
				  compute the error associated to the float *)
97
       
98
       let r = float_of_string s  in
99
       let r = Salsa.Prelude.r_of_f_aux r in
100
       Salsa.Builder.mk_cst (Float.Domain.nnew r r)
101
	 
102
      (* let r = float_of_string s  in *)
103
      (* if r = 0. then *)
104
      (* 	Salsa.Builder.mk_cst (ST.R(-. min_float, min_float),Float.ulp (ST.R(-. min_float, min_float))) *)
105
      (* else *)
106
      (* 	Salsa.Builder.mk_cst (ST.I(r*.(1.-.epsilon_float),r*.(1.+.epsilon_float)),Float.ulp (ST.I(r,r))) *)
107
    | _ -> assert false
108
end
109

    
110
module RangesInt = Ranges (FloatIntSalsa)
111

    
112
module Vars = 
113
struct
114
  module VarSet = Set.Make (struct type t = LT.var_decl let compare x y = compare x.LT.var_id y.LT.var_id end)
115
  let real_vars vs = VarSet.filter (fun v -> Types.is_real_type v.LT.var_type) vs
116
  let of_list = List.fold_left (fun s e -> VarSet.add e s) VarSet.empty 
117

    
118
  include VarSet 
119

    
120
  let remove_list (set:t) (v_list: elt list) : t = List.fold_right VarSet.remove v_list set
121
  let pp fmt vs = Utils.fprintf_list ~sep:", " Printers.pp_var fmt (VarSet.elements vs)
122
end
123

    
124

    
125

    
126

    
127

    
128

    
129

    
130

    
131

    
132

    
133
(*************************************************************************************)
134
(*                 Converting values back and forth                                  *)
135
(*************************************************************************************)
136

    
137
let rec value_t2salsa_expr constEnv vt = 
138
  let value_t2salsa_expr = value_t2salsa_expr constEnv in
139
  let res = 
140
    match vt.LT.value_desc with
141
    (* | LT.Cst(LT.Const_tag(t) as c)   ->  *)
142
    (*   Format.eprintf "v2s: cst tag@."; *)
143
    (*   if List.mem_assoc t constEnv then ( *)
144
    (* 	Format.eprintf "trouvé la constante %s: %a@ " t Printers.pp_const c; *)
145
    (* 	FloatIntSalsa.inject (List.assoc t constEnv) *)
146
    (*   ) *)
147
    (*   else (     *)
148
    (* 	Format.eprintf "Const tag %s unhandled@.@?" t ; *)
149
    (* 	raise (Salsa.Prelude.Error ("Entschuldigung6, constant tag not yet implemented")) *)
150
    (*   ) *)
151
    | LT.Cst(cst)                ->        (* Format.eprintf "v2s: cst tag 2: %a@." Printers.pp_const cst;  *)FloatIntSalsa.inject cst
152
    | LT.LocalVar(v)            
153
    | LT.StateVar(v)            ->       (* Format.eprintf "v2s: var %s@." v.LT.var_id; *) 
154
      let sel_fun = (fun (vname, _) -> v.LT.var_id = vname) in
155
      if List.exists sel_fun  constEnv then
156
	let _, cst = List.find sel_fun constEnv in
157
	FloatIntSalsa.inject cst
158
      else
159
	let id = v.LT.var_id in
160
				   Salsa.Builder.mk_id id
161
    | LT.Fun(binop, [x;y])      -> let salsaX = value_t2salsa_expr x in
162
				   let salsaY = value_t2salsa_expr y in
163
				   let op = (
164
				     let pred f x y = Salsa.Builder.mk_int_of_bool (f x y) in
165
				     match binop with
166
				     | "+" -> Salsa.Builder.mk_plus
167
				     | "-" -> Salsa.Builder.mk_minus
168
				     | "*" -> Salsa.Builder.mk_times
169
				     | "/" -> Salsa.Builder.mk_div
170
				     | "=" -> pred Salsa.Builder.mk_eq
171
				     | "<" -> pred Salsa.Builder.mk_lt
172
				     | ">" -> pred Salsa.Builder.mk_gt
173
				     | "<=" -> pred Salsa.Builder.mk_lte
174
				     | ">=" -> pred Salsa.Builder.mk_gte
175
				     | _ -> assert false
176
				   )
177
				   in
178
				   op salsaX salsaY 
179
    | LT.Fun(unop, [x])         -> let salsaX = value_t2salsa_expr x in
180
				   Salsa.Builder.mk_uminus salsaX
181

    
182
    | LT.Fun(f,_)   -> raise (Salsa.Prelude.Error 
183
				("Unhandled function "^f^" in conversion to salsa expression"))
184
    
185
    | LT.Array(_) 
186
    | LT.Access(_)
187
    | LT.Power(_)   -> raise (Salsa.Prelude.Error ("Unhandled construct in conversion to salsa expression"))
188
  in
189
  (* if debug then *)
190
  (*   Format.eprintf "value_t2salsa_expr: %a -> %a@ " *)
191
  (*     MC.pp_val vt *)
192
  (*     (fun fmt x -> Format.fprintf fmt "%s" (Salsa.Print.printExpression x)) res; *)
193
  res
194

    
195
type var_decl = { vdecl: LT.var_decl; is_local: bool }
196
module VarEnv = Map.Make (struct type t = LT.ident let compare = compare end )
197

    
198
(* let is_local_var vars_env v = *)
199
(*   try *)
200
(*   (VarEnv.find v vars_env).is_local *)
201
(*   with Not_found -> Format.eprintf "Impossible to find var %s@.@?" v; assert false *)
202

    
203
let get_var vars_env v =
204
try
205
  VarEnv.find v vars_env
206
  with Not_found -> Format.eprintf "Impossible to find var %s@.@?" v; assert false
207

    
208
let compute_vars_env m =
209
  let env = VarEnv.empty in
210
  let env = 
211
    List.fold_left 
212
      (fun accu v -> VarEnv.add v.LT.var_id {vdecl = v; is_local = false; } accu) 
213
      env 
214
      m.MC.mmemory
215
  in
216
  let env = 
217
    List.fold_left (
218
      fun accu v -> VarEnv.add v.LT.var_id {vdecl = v; is_local = true; } accu
219
    )
220
      env
221
      MC.(m.mstep.step_inputs@m.mstep.step_outputs@m.mstep.step_locals)
222
  in
223
env
224

    
225
let rec salsa_expr2value_t vars_env cst_env e  = 
226
  let salsa_expr2value_t = salsa_expr2value_t vars_env cst_env in
227
  let binop op e1 e2 t = 
228
    let x = salsa_expr2value_t e1 in
229
    let y = salsa_expr2value_t e2 in                    
230
    MC.mk_val (LT.Fun (op, [x;y])) t
231
  in
232
  match e with
233
    ST.Cst((ST.R(c,_),_),_)     -> (* We project ranges into constants. We
234
					forget about errors and provide the
235
					mean/middle value of the interval
236
				     *)
237
      let  new_float = Salsa.NumMartel.float_of_num c in
238
      (* let new_float =  *)
239
      (* 	if f1 = f2 then *)
240
      (* 	  f1 *)
241
      (* 	else *)
242
      (* 	  (f1 +. f2) /. 2.0  *)
243
      (* in *)
244
      (* Log.report ~level:3 *)
245
      (* 	(fun fmt -> Format.fprintf fmt  "projecting [%.45f, %.45f] -> %.45f@ " f1 f2 new_float); *)
246
      let cst =  
247
	let s = 
248
	  if new_float = 0. then "0." else
249
	    (* We have to convert it into our format: int * int * real *)
250
	    let _ = Format.flush_str_formatter () in
251
	    Format.fprintf Format.str_formatter "%.50f" new_float;
252
	    Format.flush_str_formatter () 
253
	in
254
	Parser_lustre.signed_const Lexer_lustre.token (Lexing.from_string s) 
255
      in
256
      MC.mk_val (LT.Cst(cst)) Type_predef.type_real
257
  | ST.Id(id, _)          -> 
258
    (* Format.eprintf "Looking for id=%s@.@?" id; *)
259
     if List.mem_assoc id cst_env then (
260
       let cst = List.assoc id cst_env in
261
      (* Format.eprintf "Found cst = %a@.@?" Printers.pp_const cst; *)
262
       MC.mk_val (LT.Cst cst) Type_predef.type_real
263
     )
264
     else
265
      (* if is_const salsa_label then *)
266
      (*   MC.Cst(LT.Const_tag(get_const salsa_label)) *)
267
      (* else *) 
268
       let var_id = try get_var vars_env id with Not_found -> assert false in
269
       if var_id.is_local then
270
	 MC.mk_val (LT.LocalVar(var_id.vdecl)) var_id.vdecl.LT.var_type
271
       else
272
	 MC.mk_val (LT.StateVar(var_id.vdecl)) var_id.vdecl.LT.var_type
273
  | ST.Plus(x, y, _)               -> binop "+" x y Type_predef.type_real
274
  | ST.Minus(x, y, _)              -> binop "-" x y Type_predef.type_real
275
  | ST.Times(x, y, _)              -> binop "*" x y Type_predef.type_real
276
  | ST.Div(x, y, _)                -> binop "/" x y Type_predef.type_real
277
  | ST.Uminus(x,_)                 -> let x = salsa_expr2value_t x in
278
				      MC.mk_val (LT.Fun("uminus",[x])) Type_predef.type_real
279
  | ST.IntOfBool(ST.Eq(x, y, _),_) -> binop "=" x y Type_predef.type_bool
280
  | ST.IntOfBool(ST.Lt(x,y,_),_)   -> binop "<" x y Type_predef.type_bool
281
  | ST.IntOfBool(ST.Gt(x,y,_),_)   -> binop ">" x y Type_predef.type_bool
282
  | ST.IntOfBool(ST.Lte(x,y,_),_)  -> binop "<=" x y Type_predef.type_bool
283
  | ST.IntOfBool(ST.Gte(x,y,_),_)  -> binop ">=" x y Type_predef.type_bool
284
  | _      -> raise (Salsa.Prelude.Error "Entschuldigung, salsaExpr2value_t case not yet implemented")
285

    
286

    
287
let rec get_salsa_free_vars vars_env constEnv absenv e =
288
  let f = get_salsa_free_vars vars_env constEnv absenv in
289
  match e with
290
  | ST.Id (id, _) -> 
291
    if not (List.mem_assoc id absenv) && not (List.mem_assoc id constEnv) then
292
      Vars.singleton ((try VarEnv.find id vars_env with Not_found -> assert false).vdecl) 
293
    else
294
      Vars.empty
295
  | ST.Plus(x, y, _)  
296
  | ST.Minus(x, y, _)
297
  | ST.Times(x, y, _)
298
  | ST.Div(x, y, _)
299
  | ST.IntOfBool(ST.Eq(x, y, _),_) 
300
  | ST.IntOfBool(ST.Lt(x,y,_),_)   
301
  | ST.IntOfBool(ST.Gt(x,y,_),_)   
302
  | ST.IntOfBool(ST.Lte(x,y,_),_)  
303
  | ST.IntOfBool(ST.Gte(x,y,_),_)  
304
    -> Vars.union (f x) (f y)
305
  | ST.Uminus(x,_)    -> f x
306
  | ST.Cst _ -> Vars.empty
307
  | _ -> assert false
308

    
309

    
310
module FormalEnv =
311
struct
312
  type fe_t = (LT.ident, (int * LT.value_t)) Hashtbl.t
313
  let cpt = ref 0
314

    
315
  exception NoDefinition of LT.var_decl
316
  (* Returns the expression associated to v in env *)
317
  let get_def (env: fe_t) v = 
318
    try 
319
      snd (Hashtbl.find env v.LT.var_id) 
320
    with Not_found -> raise (NoDefinition v)
321

    
322
  let fold f = Hashtbl.fold (fun k (_,v) accu -> f k v accu)
323
      
324
  let to_salsa constEnv formalEnv = 
325
    fold (fun id expr accu ->
326
      (id, value_t2salsa_expr constEnv expr)::accu
327
    ) formalEnv [] 
328

    
329
  let def constEnv vars_env (env: fe_t) d expr = 
330
    incr cpt;
331
    let fresh = Hashtbl.copy env in
332
    let expr_salsa = value_t2salsa_expr constEnv expr in
333
    let salsa_env = to_salsa constEnv env in
334
    let expr_salsa, _ = Salsa.Rewrite.substVars expr_salsa salsa_env 0 in
335
    let expr_salsa = Salsa.Analyzer.evalPartExpr expr_salsa salsa_env ([] (* no blacklisted vars *)) ([] (*no arrays *)) in
336
    let expr_lustrec = salsa_expr2value_t vars_env [] expr_salsa in
337
    Hashtbl.add fresh d.LT.var_id (!cpt, expr_lustrec); fresh
338

    
339
  let empty (): fe_t = Hashtbl.create 13
340

    
341
  let pp fmt env = pp_hash ~sep:";" (fun k (_,v) fmt -> Format.fprintf fmt "%s -> %a" k MC.pp_val v) fmt env
342

    
343

    
344
  let get_sort_fun env =
345
    let order = Hashtbl.fold (fun k (cpt, _) accu -> (k,cpt)::accu) env [] in
346
    fun v1 v2 -> 
347
      if List.mem_assoc v1.LT.var_id order && List.mem_assoc v2.LT.var_id order then
348
	if (List.assoc v1.LT.var_id order) <= (List.assoc v2.LT.var_id order) then 
349
	  -1
350
	else 
351
	  1
352
      else
353
	assert false
354
end
355

    
356
     
357
(* Local Variables: *)
358
(* compile-command:"make -C ../../.." *)
359
(* End: *)