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
|
module type VALUE = sig
|
16
|
type t
|
17
|
|
18
|
val union : t -> t -> t
|
19
|
|
20
|
val pp : Format.formatter -> t -> unit
|
21
|
|
22
|
val leq : t -> t -> bool
|
23
|
end
|
24
|
|
25
|
module Ranges =
|
26
|
functor
|
27
|
(Value : VALUE)
|
28
|
->
|
29
|
struct
|
30
|
module Value = Value
|
31
|
|
32
|
type t = Value.t
|
33
|
|
34
|
type r_t = (LT.ident, Value.t) Hashtbl.t
|
35
|
|
36
|
let empty : r_t = Hashtbl.create 13
|
37
|
|
38
|
(* 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
|
|
44
|
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
|
|
86
|
let to_abstract_env ranges =
|
87
|
Hashtbl.fold (fun id value accu -> (id, value) :: accu) ranges []
|
88
|
end
|
89
|
|
90
|
module FloatIntSalsa = struct
|
91
|
type t = ST.abstractValue
|
92
|
|
93
|
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
|
|
97
|
(* 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
|
|
102
|
| _ -> assert false *)
|
103
|
let union v1 v2 = Salsa.Float.Domain.join v1 v2
|
104
|
|
105
|
(* 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
|
|
137
|
module RangesInt = Ranges (FloatIntSalsa)
|
138
|
|
139
|
module Vars = struct
|
140
|
module VarSet = Set.Make (struct
|
141
|
type t = LT.var_decl
|
142
|
|
143
|
let compare x y = compare x.LT.var_id y.LT.var_id
|
144
|
end)
|
145
|
|
146
|
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
|
|
160
|
(*************************************************************************************)
|
161
|
(* Converting values back and forth *)
|
162
|
(*************************************************************************************)
|
163
|
|
164
|
let rec value_t2salsa_expr constEnv vt =
|
165
|
let value_t2salsa_expr = value_t2salsa_expr constEnv in
|
166
|
let res =
|
167
|
match vt.MT.value_desc with
|
168
|
(* | 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
|
(* 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
|
else
|
189
|
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
|
in
|
231
|
(* if debug then *)
|
232
|
(* Format.eprintf "value_t2salsa_expr: %a -> %a@ " *)
|
233
|
(* MC.pp_val vt *)
|
234
|
(* (fun fmt x -> Format.fprintf fmt "%s" (Salsa.Print.printExpression x)) res; *)
|
235
|
res
|
236
|
|
237
|
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
|
|
245
|
(* let is_local_var vars_env v = *)
|
246
|
(* try *)
|
247
|
(* (VarEnv.find v vars_env).is_local *)
|
248
|
(* with Not_found -> Format.eprintf "Impossible to find var %s@.@?" v; assert
|
249
|
false *)
|
250
|
|
251
|
let get_var vars_env v =
|
252
|
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
|
|
260
|
let compute_vars_env m =
|
261
|
let env = VarEnv.empty in
|
262
|
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
|
in
|
268
|
let env =
|
269
|
List.fold_left
|
270
|
(fun accu v -> VarEnv.add v.LT.var_id { vdecl = v; is_local = true } accu)
|
271
|
env
|
272
|
MC.(
|
273
|
m.MT.mstep.MT.step_inputs @ m.MT.mstep.MT.step_outputs
|
274
|
@ m.MT.mstep.MT.step_locals)
|
275
|
in
|
276
|
env
|
277
|
|
278
|
let rec salsa_expr2value_t vars_env cst_env e =
|
279
|
(* let e = Float.evalPartExpr e [] [] in *)
|
280
|
let salsa_expr2value_t = salsa_expr2value_t vars_env cst_env in
|
281
|
let binop op e1 e2 t =
|
282
|
let x = salsa_expr2value_t e1 in
|
283
|
let y = salsa_expr2value_t e2 in
|
284
|
MC.mk_val (MT.Fun (op, [ x; y ])) t
|
285
|
in
|
286
|
match e with
|
287
|
| 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
|
let new_float = Salsa.Float.Domain.to_float abs_val in
|
291
|
(* 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
|
in
|
311
|
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
|
(* Format.eprintf "Looking for id=%s@.@?" id; *)
|
316
|
if List.mem_assoc id cst_env then
|
317
|
let cst = List.assoc id cst_env in
|
318
|
(* Format.eprintf "Found cst = %a@.@?" Printers.pp_const cst; *)
|
319
|
MC.mk_val (MT.Cst cst) Type_predef.type_real
|
320
|
else
|
321
|
(* if is_const salsa_label then *)
|
322
|
(* MC.Cst(LT.Const_tag(get_const salsa_label)) *)
|
323
|
(* 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
|
|
352
|
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
|
| 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
|
let cpt = ref 0
|
381
|
|
382
|
exception NoDefinition of LT.var_decl
|
383
|
|
384
|
(* Returns the expression associated to v in env *)
|
385
|
let get_def (env : fe_t) v =
|
386
|
try snd (Hashtbl.find env v.LT.var_id)
|
387
|
with Not_found -> raise (NoDefinition v)
|
388
|
|
389
|
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
|
|
396
|
let def constEnv vars_env (env : fe_t) d expr =
|
397
|
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
|
let expr_salsa =
|
403
|
Salsa.Analyzer.evalPartExpr expr_salsa salsa_env []
|
404
|
(* no blacklisted vars *)
|
405
|
[]
|
406
|
(*no arrays *)
|
407
|
in
|
408
|
let expr_lustrec = salsa_expr2value_t vars_env [] expr_salsa in
|
409
|
Hashtbl.add fresh d.LT.var_id (!cpt, expr_lustrec);
|
410
|
fresh
|
411
|
|
412
|
let empty () : fe_t = Hashtbl.create 13
|
413
|
|
414
|
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
|
|
419
|
let get_sort_fun env =
|
420
|
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
|
end
|
429
|
|
430
|
(* Local Variables: *)
|
431
|
(* compile-command:"make -C ../../.." *)
|
432
|
(* End: *)
|