Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/plugins/salsa/salsaDatatypes.ml | ||
---|---|---|
5 | 5 |
|
6 | 6 |
let debug = ref false |
7 | 7 |
|
8 |
let _ = Salsa.Prelude.sliceSize := 5
|
|
9 |
|
|
10 |
let pp_hash ~sep f fmt r =
|
|
8 |
let _ = Salsa.Prelude.sliceSize := 5 |
|
9 |
|
|
10 |
let pp_hash ~sep f fmt r = |
|
11 | 11 |
Format.fprintf fmt "[@[<v>"; |
12 | 12 |
Hashtbl.iter (fun k v -> Format.fprintf fmt "%t%s@ " (f k v) sep) r; |
13 |
Format.fprintf fmt "]@]"; |
|
14 |
|
|
13 |
Format.fprintf fmt "]@]" |
|
15 | 14 |
|
16 |
module type VALUE = |
|
17 |
sig |
|
15 |
module type VALUE = sig |
|
18 | 16 |
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 | 17 |
|
18 |
val union : t -> t -> t |
|
85 | 19 |
|
86 |
let to_abstract_env ranges = |
|
87 |
Hashtbl.fold |
|
88 |
(fun id value accu -> (id,value)::accu) |
|
89 |
ranges |
|
90 |
[] |
|
20 |
val pp : Format.formatter -> t -> unit |
|
21 |
|
|
22 |
val leq : t -> t -> bool |
|
91 | 23 |
end |
92 | 24 |
|
93 |
module FloatIntSalsa = |
|
94 |
struct |
|
95 |
type t = ST.abstractValue |
|
25 |
module Ranges = |
|
26 |
functor |
|
27 |
(Value : VALUE) |
|
28 |
-> |
|
29 |
struct |
|
30 |
module Value = Value |
|
96 | 31 |
|
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 r -> (* 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 = Real.to_q r in |
|
120 |
Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_q 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 |
|
32 |
type t = Value.t |
|
131 | 33 |
|
132 |
let leq = (* Salsa.Float.feSseq *) Salsa.Float.Domain.leq |
|
133 |
end |
|
34 |
type r_t = (LT.ident, Value.t) Hashtbl.t |
|
134 | 35 |
|
135 |
module RangesInt = Ranges (FloatIntSalsa)
|
|
36 |
let empty : r_t = Hashtbl.create 13
|
|
136 | 37 |
|
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
|
|
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 *)
|
|
142 | 43 |
|
143 |
include VarSet |
|
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 |
|
144 | 85 |
|
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 |
|
86 |
let to_abstract_env ranges =
|
|
87 |
Hashtbl.fold (fun id value accu -> (id, value) :: accu) ranges []
|
|
88 |
end
|
|
148 | 89 |
|
90 |
module FloatIntSalsa = struct |
|
91 |
type t = ST.abstractValue |
|
149 | 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 |
|
150 | 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 "???" |
|
151 | 101 |
|
102 |
| _ -> assert false *) |
|
103 |
let union v1 v2 = Salsa.Float.Domain.join v1 v2 |
|
152 | 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 |
|
153 | 136 |
|
137 |
module RangesInt = Ranges (FloatIntSalsa) |
|
154 | 138 |
|
139 |
module Vars = struct |
|
140 |
module VarSet = Set.Make (struct |
|
141 |
type t = LT.var_decl |
|
155 | 142 |
|
143 |
let compare x y = compare x.LT.var_id y.LT.var_id |
|
144 |
end) |
|
156 | 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 |
|
157 | 159 |
|
158 | 160 |
(*************************************************************************************) |
159 |
(* Converting values back and forth *)
|
|
161 |
(* Converting values back and forth *)
|
|
160 | 162 |
(*************************************************************************************) |
161 | 163 |
|
162 |
let rec value_t2salsa_expr constEnv vt =
|
|
164 |
let rec value_t2salsa_expr constEnv vt = |
|
163 | 165 |
let value_t2salsa_expr = value_t2salsa_expr constEnv in |
164 |
let res =
|
|
166 |
let res = |
|
165 | 167 |
match vt.MT.value_desc with |
166 | 168 |
(* | LT.Cst(LT.Const_tag(t) as c) -> *) |
167 | 169 |
(* Format.eprintf "v2s: cst tag@."; *) |
... | ... | |
171 | 173 |
(* ) *) |
172 | 174 |
(* else ( *) |
173 | 175 |
(* 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 |
|
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 |
|
182 | 188 |
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")) |
|
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") |
|
212 | 230 |
in |
213 | 231 |
(* if debug then *) |
214 | 232 |
(* Format.eprintf "value_t2salsa_expr: %a -> %a@ " *) |
215 | 233 |
(* MC.pp_val vt *) |
216 |
(* (fun fmt x -> Format.fprintf fmt "%s" (Salsa.Print.printExpression x)) res; *)
|
|
234 |
(* (fun fmt x -> Format.fprintf fmt "%s" (Salsa.Print.printExpression x)) res; *) |
|
217 | 235 |
res |
218 | 236 |
|
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 ) |
|
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) |
|
221 | 244 |
|
222 | 245 |
(* let is_local_var vars_env v = *) |
223 | 246 |
(* try *) |
224 | 247 |
(* (VarEnv.find v vars_env).is_local *) |
225 |
(* with Not_found -> Format.eprintf "Impossible to find var %s@.@?" v; assert false *) |
|
248 |
(* with Not_found -> Format.eprintf "Impossible to find var %s@.@?" v; assert |
|
249 |
false *) |
|
226 | 250 |
|
227 | 251 |
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 |
|
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 |
|
233 | 259 |
|
234 | 260 |
let compute_vars_env m = |
235 | 261 |
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 |
|
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
|
|
241 | 267 |
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 |
) |
|
268 |
let env = |
|
269 |
List.fold_left |
|
270 |
(fun accu v -> VarEnv.add v.LT.var_id { vdecl = v; is_local = true } accu) |
|
246 | 271 |
env |
247 |
MC.(m.MT.mstep.MT.step_inputs@m.MT.mstep.MT.step_outputs@m.MT.mstep.MT.step_locals) |
|
272 |
MC.( |
|
273 |
m.MT.mstep.MT.step_inputs @ m.MT.mstep.MT.step_outputs |
|
274 |
@ m.MT.mstep.MT.step_locals) |
|
248 | 275 |
in |
249 |
env |
|
276 |
env
|
|
250 | 277 |
|
251 |
let rec salsa_expr2value_t vars_env cst_env e =
|
|
252 |
(* let e = Float.evalPartExpr e [] [] in *)
|
|
278 |
let rec salsa_expr2value_t vars_env cst_env e =
|
|
279 |
(* let e = Float.evalPartExpr e [] [] in *) |
|
253 | 280 |
let salsa_expr2value_t = salsa_expr2value_t vars_env cst_env in |
254 |
let binop op e1 e2 t =
|
|
281 |
let binop op e1 e2 t = |
|
255 | 282 |
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
|
|
283 |
let y = salsa_expr2value_t e2 in |
|
284 |
MC.mk_val (MT.Fun (op, [ x; y ])) t
|
|
258 | 285 |
in |
259 | 286 |
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 |
*) |
|
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 *) |
|
264 | 290 |
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)
|
|
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 ()
|
|
284 | 310 |
in |
285 |
MC.mk_val (MT.Cst(cst)) Type_predef.type_real |
|
286 |
| ST.Id(id, _) -> |
|
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, _) -> |
|
287 | 315 |
(* 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
|
|
316 |
if List.mem_assoc id cst_env then
|
|
317 |
let cst = List.assoc id cst_env in |
|
290 | 318 |
(* Format.eprintf "Found cst = %a@.@?" Printers.pp_const cst; *) |
291 |
MC.mk_val (MT.Cst cst) Type_predef.type_real |
|
292 |
) |
|
293 |
else |
|
319 |
MC.mk_val (MT.Cst cst) Type_predef.type_real |
|
320 |
else |
|
294 | 321 |
(* if is_const salsa_label then *) |
295 | 322 |
(* 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 |
|
|
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") |
|
313 | 351 |
|
314 | 352 |
let rec get_salsa_free_vars vars_env constEnv absenv e = |
315 | 353 |
let f = get_salsa_free_vars vars_env constEnv absenv in |
316 | 354 |
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 |
|
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 |
|
|
340 | 380 |
let cpt = ref 0 |
341 | 381 |
|
342 | 382 |
exception NoDefinition of LT.var_decl |
383 |
|
|
343 | 384 |
(* 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) |
|
385 |
let get_def (env : fe_t) v = |
|
386 |
try snd (Hashtbl.find env v.LT.var_id) |
|
347 | 387 |
with Not_found -> raise (NoDefinition v) |
348 | 388 |
|
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 []
|
|
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 []
|
|
355 | 395 |
|
356 |
let def constEnv vars_env (env: fe_t) d expr =
|
|
396 |
let def constEnv vars_env (env : fe_t) d expr =
|
|
357 | 397 |
incr cpt; |
358 | 398 |
let fresh = Hashtbl.copy env in |
359 | 399 |
let expr_salsa = value_t2salsa_expr constEnv expr in |
360 | 400 |
let salsa_env = to_salsa constEnv env in |
361 | 401 |
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 |
|
402 |
let expr_salsa = |
|
403 |
Salsa.Analyzer.evalPartExpr expr_salsa salsa_env [] |
|
404 |
(* no blacklisted vars *) |
|
405 |
[] |
|
406 |
(*no arrays *) |
|
407 |
in |
|
363 | 408 |
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 |
|
409 |
Hashtbl.add fresh d.LT.var_id (!cpt, expr_lustrec); |
|
410 |
fresh |
|
367 | 411 |
|
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
|
|
412 |
let empty () : fe_t = Hashtbl.create 13
|
|
369 | 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 |
|
370 | 418 |
|
371 | 419 |
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 |
|
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 |
|
381 | 428 |
end |
382 | 429 |
|
383 |
|
|
384 | 430 |
(* Local Variables: *) |
385 | 431 |
(* compile-command:"make -C ../../.." *) |
386 | 432 |
(* End: *) |
Also available in: Unified diff
reformatting