1
|
module LT = Lustre_types
|
2
|
module MT = Machine_code_types
|
3
|
module MC = Machine_code_common
|
4
|
module ST = Salsa.Types
|
5
|
|
6
|
let debug = ref false
|
7
|
|
8
|
let _ = Salsa.Prelude.sliceSize := 5
|
9
|
|
10
|
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
|
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
|
module Ranges =
|
25
|
functor (Value: VALUE) ->
|
26
|
struct
|
27
|
module Value = Value
|
28
|
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
|
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
|
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
|
(* Format.eprintf "Mergeing rangesint %a with %a@." pp ranges1 pp ranges2; *)
|
69
|
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
|
(* Format.eprintf "Merge result %a@." pp ranges; *)
|
83
|
ranges
|
84
|
|
85
|
|
86
|
let to_abstract_env ranges =
|
87
|
Hashtbl.fold
|
88
|
(fun id value accu -> (id,value)::accu)
|
89
|
ranges
|
90
|
[]
|
91
|
end
|
92
|
|
93
|
module FloatIntSalsa =
|
94
|
struct
|
95
|
type t = ST.abstractValue
|
96
|
|
97
|
let pp fmt ((f,r):t) =
|
98
|
let fs, rs = (Salsa.Float.Domain.print (f,r)) in
|
99
|
Format.fprintf fmt "%s + %s" fs rs
|
100
|
(* match f, r with
|
101
|
| ST.I(a,b), ST.J(c,d) ->
|
102
|
Format.fprintf fmt "[%f, %f] + [%s, %s]" a b (Num.string_of_num c) (Num.string_of_num d)
|
103
|
| 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
|
*)
|
108
|
let union v1 v2 = Salsa.Float.Domain.join v1 v2
|
109
|
(* match v1, v2 with
|
110
|
|(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
|
*)
|
114
|
let inject cst = match cst with
|
115
|
| LT.Const_int(i) -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_int i)
|
116
|
| LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather
|
117
|
compute the error associated to the float *)
|
118
|
(* 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
|
|
122
|
(* let r = Salsa.Prelude.r_of_f_aux r in *)
|
123
|
(* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *)
|
124
|
|
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
|
| _ -> assert false
|
131
|
|
132
|
let leq = (* Salsa.Float.feSseq *) Salsa.Float.Domain.leq
|
133
|
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
|
match vt.MT.value_desc with
|
166
|
(* | 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
|
| MT.Cst(cst) -> (* Format.eprintf "v2s: cst tag 2: %a@." Printers.pp_const cst; *)FloatIntSalsa.inject cst
|
177
|
| MT.Var(v) -> (* Format.eprintf "v2s: var %s@." v.LT.var_id; *)
|
178
|
let sel_fun = (fun (vname, _) -> v.LT.var_id = vname) in
|
179
|
if List.exists sel_fun constEnv then
|
180
|
let _, cst = List.find sel_fun constEnv in
|
181
|
FloatIntSalsa.inject cst
|
182
|
else
|
183
|
let id = v.LT.var_id in
|
184
|
Salsa.Builder.mk_id id
|
185
|
| MT.Fun(binop, [x;y]) -> let salsaX = value_t2salsa_expr x in
|
186
|
let salsaY = value_t2salsa_expr y in
|
187
|
let op = (
|
188
|
let pred f x y = Salsa.Builder.mk_int_of_bool (f x y) in
|
189
|
match binop with
|
190
|
| "+" -> Salsa.Builder.mk_plus
|
191
|
| "-" -> Salsa.Builder.mk_minus
|
192
|
| "*" -> Salsa.Builder.mk_times
|
193
|
| "/" -> Salsa.Builder.mk_div
|
194
|
| "=" -> pred Salsa.Builder.mk_eq
|
195
|
| "<" -> pred Salsa.Builder.mk_lt
|
196
|
| ">" -> pred Salsa.Builder.mk_gt
|
197
|
| "<=" -> pred Salsa.Builder.mk_lte
|
198
|
| ">=" -> pred Salsa.Builder.mk_gte
|
199
|
| _ -> assert false
|
200
|
)
|
201
|
in
|
202
|
op salsaX salsaY
|
203
|
| MT.Fun(unop, [x]) -> let salsaX = value_t2salsa_expr x in
|
204
|
Salsa.Builder.mk_uminus salsaX
|
205
|
|
206
|
| MT.Fun(f,_) -> raise (Salsa.Prelude.Error
|
207
|
("Unhandled function "^f^" in conversion to salsa expression"))
|
208
|
|
209
|
| MT.Array(_)
|
210
|
| MT.Access(_)
|
211
|
| MT.Power(_) -> raise (Salsa.Prelude.Error ("Unhandled construct in conversion to salsa expression"))
|
212
|
in
|
213
|
(* if debug then *)
|
214
|
(* Format.eprintf "value_t2salsa_expr: %a -> %a@ " *)
|
215
|
(* MC.pp_val vt *)
|
216
|
(* (fun fmt x -> Format.fprintf fmt "%s" (Salsa.Print.printExpression x)) res; *)
|
217
|
res
|
218
|
|
219
|
type var_decl = { vdecl: LT.var_decl; is_local: bool }
|
220
|
module VarEnv = Map.Make (struct type t = LT.ident let compare = compare end )
|
221
|
|
222
|
(* let is_local_var vars_env v = *)
|
223
|
(* try *)
|
224
|
(* (VarEnv.find v vars_env).is_local *)
|
225
|
(* with Not_found -> Format.eprintf "Impossible to find var %s@.@?" v; assert false *)
|
226
|
|
227
|
let get_var vars_env v =
|
228
|
try
|
229
|
VarEnv.find v vars_env
|
230
|
with Not_found -> Format.eprintf "Impossible to find var %s in var env %a@ " v
|
231
|
(Utils.fprintf_list ~sep:", " (fun fmt (id, _) -> Format.pp_print_string fmt id)) (VarEnv.bindings vars_env)
|
232
|
; assert false
|
233
|
|
234
|
let compute_vars_env m =
|
235
|
let env = VarEnv.empty in
|
236
|
let env =
|
237
|
List.fold_left
|
238
|
(fun accu v -> VarEnv.add v.LT.var_id {vdecl = v; is_local = false; } accu)
|
239
|
env
|
240
|
m.MT.mmemory
|
241
|
in
|
242
|
let env =
|
243
|
List.fold_left (
|
244
|
fun accu v -> VarEnv.add v.LT.var_id {vdecl = v; is_local = true; } accu
|
245
|
)
|
246
|
env
|
247
|
MC.(m.MT.mstep.MT.step_inputs@m.MT.mstep.MT.step_outputs@m.MT.mstep.MT.step_locals)
|
248
|
in
|
249
|
env
|
250
|
|
251
|
let rec salsa_expr2value_t vars_env cst_env e =
|
252
|
(* let e = Float.evalPartExpr e [] [] in *)
|
253
|
let salsa_expr2value_t = salsa_expr2value_t vars_env cst_env in
|
254
|
let binop op e1 e2 t =
|
255
|
let x = salsa_expr2value_t e1 in
|
256
|
let y = salsa_expr2value_t e2 in
|
257
|
MC.mk_val (MT.Fun (op, [x;y])) t
|
258
|
in
|
259
|
match e with
|
260
|
ST.Cst(abs_val,_) -> (* We project ranges into constants. We
|
261
|
forget about errors and provide the
|
262
|
mean/middle value of the interval
|
263
|
*)
|
264
|
let new_float = Salsa.Float.Domain.to_float abs_val in
|
265
|
(* let new_float = Salsa.NumMartel.float_of_num c in *)
|
266
|
(* let new_float = *)
|
267
|
(* if f1 = f2 then *)
|
268
|
(* f1 *)
|
269
|
(* else *)
|
270
|
(* (f1 +. f2) /. 2.0 *)
|
271
|
(* in *)
|
272
|
(* Log.report ~level:3 *)
|
273
|
(* (fun fmt -> Format.fprintf fmt "projecting [%.45f, %.45f] -> %.45f@ " f1 f2 new_float); *)
|
274
|
let cst =
|
275
|
let s =
|
276
|
if new_float = 0. then "0." else
|
277
|
(* We have to convert it into our format: int * int * real *)
|
278
|
(* string_of_float new_float *)
|
279
|
let _ = Format.flush_str_formatter () in
|
280
|
Format.fprintf Format.str_formatter "%.11f" new_float;
|
281
|
Format.flush_str_formatter ()
|
282
|
in
|
283
|
Parser_lustre.signed_const Lexer_lustre.token (Lexing.from_string s)
|
284
|
in
|
285
|
MC.mk_val (MT.Cst(cst)) Type_predef.type_real
|
286
|
| ST.Id(id, _) ->
|
287
|
(* Format.eprintf "Looking for id=%s@.@?" id; *)
|
288
|
if List.mem_assoc id cst_env then (
|
289
|
let cst = List.assoc id cst_env in
|
290
|
(* Format.eprintf "Found cst = %a@.@?" Printers.pp_const cst; *)
|
291
|
MC.mk_val (MT.Cst cst) Type_predef.type_real
|
292
|
)
|
293
|
else
|
294
|
(* if is_const salsa_label then *)
|
295
|
(* MC.Cst(LT.Const_tag(get_const salsa_label)) *)
|
296
|
(* else *)
|
297
|
let var_id = try get_var vars_env id with Not_found -> assert false in
|
298
|
MC.mk_val (MT.Var(var_id.vdecl)) var_id.vdecl.LT.var_type
|
299
|
| ST.Plus(x, y, _) -> binop "+" x y Type_predef.type_real
|
300
|
| ST.Minus(x, y, _) -> binop "-" x y Type_predef.type_real
|
301
|
| ST.Times(x, y, _) -> binop "*" x y Type_predef.type_real
|
302
|
| ST.Div(x, y, _) -> binop "/" x y Type_predef.type_real
|
303
|
| ST.Uminus(x,_) -> let x = salsa_expr2value_t x in
|
304
|
MC.mk_val (MT.Fun("uminus",[x])) Type_predef.type_real
|
305
|
| ST.IntOfBool(ST.Eq(x, y, _),_) -> binop "=" x y Type_predef.type_bool
|
306
|
| ST.IntOfBool(ST.Lt(x,y,_),_) -> binop "<" x y Type_predef.type_bool
|
307
|
| ST.IntOfBool(ST.Gt(x,y,_),_) -> binop ">" x y Type_predef.type_bool
|
308
|
| ST.IntOfBool(ST.Lte(x,y,_),_) -> binop "<=" x y Type_predef.type_bool
|
309
|
| ST.IntOfBool(ST.Gte(x,y,_),_) -> binop ">=" x y Type_predef.type_bool
|
310
|
| _ -> raise (Salsa.Prelude.Error "Entschuldigung, salsaExpr2value_t case not yet implemented")
|
311
|
|
312
|
|
313
|
|
314
|
let rec get_salsa_free_vars vars_env constEnv absenv e =
|
315
|
let f = get_salsa_free_vars vars_env constEnv absenv in
|
316
|
match e with
|
317
|
| ST.Id (id, _) ->
|
318
|
if not (List.mem_assoc id absenv) && not (List.mem_assoc id constEnv) then
|
319
|
Vars.singleton ((try VarEnv.find id vars_env with Not_found -> assert false).vdecl)
|
320
|
else
|
321
|
Vars.empty
|
322
|
| ST.Plus(x, y, _)
|
323
|
| ST.Minus(x, y, _)
|
324
|
| ST.Times(x, y, _)
|
325
|
| ST.Div(x, y, _)
|
326
|
| ST.IntOfBool(ST.Eq(x, y, _),_)
|
327
|
| ST.IntOfBool(ST.Lt(x,y,_),_)
|
328
|
| ST.IntOfBool(ST.Gt(x,y,_),_)
|
329
|
| ST.IntOfBool(ST.Lte(x,y,_),_)
|
330
|
| ST.IntOfBool(ST.Gte(x,y,_),_)
|
331
|
-> Vars.union (f x) (f y)
|
332
|
| ST.Uminus(x,_) -> f x
|
333
|
| ST.Cst _ -> Vars.empty
|
334
|
| _ -> assert false
|
335
|
|
336
|
|
337
|
module FormalEnv =
|
338
|
struct
|
339
|
type fe_t = (LT.ident, (int * MT.value_t)) Hashtbl.t
|
340
|
let cpt = ref 0
|
341
|
|
342
|
exception NoDefinition of LT.var_decl
|
343
|
(* Returns the expression associated to v in env *)
|
344
|
let get_def (env: fe_t) v =
|
345
|
try
|
346
|
snd (Hashtbl.find env v.LT.var_id)
|
347
|
with Not_found -> raise (NoDefinition v)
|
348
|
|
349
|
let fold f = Hashtbl.fold (fun k (_,v) accu -> f k v accu)
|
350
|
|
351
|
let to_salsa constEnv formalEnv =
|
352
|
fold (fun id expr accu ->
|
353
|
(id, value_t2salsa_expr constEnv expr)::accu
|
354
|
) formalEnv []
|
355
|
|
356
|
let def constEnv vars_env (env: fe_t) d expr =
|
357
|
incr cpt;
|
358
|
let fresh = Hashtbl.copy env in
|
359
|
let expr_salsa = value_t2salsa_expr constEnv expr in
|
360
|
let salsa_env = to_salsa constEnv env in
|
361
|
let expr_salsa, _ = Salsa.Rewrite.substVars expr_salsa salsa_env 0 in
|
362
|
let expr_salsa = Salsa.Analyzer.evalPartExpr expr_salsa salsa_env ([] (* no blacklisted vars *)) ([] (*no arrays *)) in
|
363
|
let expr_lustrec = salsa_expr2value_t vars_env [] expr_salsa in
|
364
|
Hashtbl.add fresh d.LT.var_id (!cpt, expr_lustrec); fresh
|
365
|
|
366
|
let empty (): fe_t = Hashtbl.create 13
|
367
|
|
368
|
let pp m fmt env = pp_hash ~sep:";@ " (fun k (_,v) fmt -> Format.fprintf fmt "%s -> %a" k (MC.pp_val m) v) fmt env
|
369
|
|
370
|
|
371
|
let get_sort_fun env =
|
372
|
let order = Hashtbl.fold (fun k (cpt, _) accu -> (k,cpt)::accu) env [] in
|
373
|
fun v1 v2 ->
|
374
|
if List.mem_assoc v1.LT.var_id order && List.mem_assoc v2.LT.var_id order then
|
375
|
if (List.assoc v1.LT.var_id order) <= (List.assoc v2.LT.var_id order) then
|
376
|
-1
|
377
|
else
|
378
|
1
|
379
|
else
|
380
|
assert false
|
381
|
end
|
382
|
|
383
|
|
384
|
(* Local Variables: *)
|
385
|
(* compile-command:"make -C ../../.." *)
|
386
|
(* End: *)
|