Revision 9a9058f4
Added by Pierre-Loïc Garoche over 5 years ago
| src/corelang.ml | ||
|---|---|---|
| 516 | 516 |
List.sort (fun (t, _) (t', _) -> compare t t') hl |
| 517 | 517 |
|
| 518 | 518 |
let num_10 = Num.num_of_int 10 |
| 519 |
|
|
| 519 |
|
|
| 520 |
let cst_real_to_num n i = |
|
| 521 |
Num.(n // (num_10 **/ (num_of_int i))) |
|
| 522 |
|
|
| 520 | 523 |
let rec is_eq_const c1 c2 = |
| 521 | 524 |
match c1, c2 with |
| 522 | 525 |
| Const_real (n1, i1, _), Const_real (n2, i2, _) |
| 523 |
-> Num.(let n1 = n1 // (num_10 **/ (num_of_int i1)) in
|
|
| 524 |
let n2 = n2 // (num_10 **/ (num_of_int i2)) in
|
|
| 525 |
eq_num n1 n2)
|
|
| 526 |
-> let n1 = cst_real_to_num n1 i1 in
|
|
| 527 |
let n2 = cst_real_to_num n2 i2 in
|
|
| 528 |
Num.eq_num n1 n2
|
|
| 526 | 529 |
| Const_struct lcl1, Const_struct lcl2 |
| 527 | 530 |
-> List.length lcl1 = List.length lcl2 |
| 528 | 531 |
&& List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2 |
| src/corelang.mli | ||
|---|---|---|
| 165 | 165 |
|
| 166 | 166 |
val reset_cpt_fresh: unit -> unit |
| 167 | 167 |
val mk_fresh_var: node_desc -> Location.t -> Types.type_expr -> Clocks.clock_expr -> var_decl |
| 168 |
|
|
| 169 |
|
|
| 170 |
(* Extract a num to describe a real constant *) |
|
| 171 |
val cst_real_to_num: Num.num -> int -> Num.num |
|
| 168 | 172 |
(* Local Variables: *) |
| 169 | 173 |
(* compile-command:"make -C .." *) |
| 170 | 174 |
(* End: *) |
| src/plugins/salsa/machine_salsa_opt.ml | ||
|---|---|---|
| 98 | 98 |
let fresh_id = "toto" in (* TODO more meaningful name *) |
| 99 | 99 |
|
| 100 | 100 |
let abstractEnv = RangesInt.to_abstract_env ranges in |
| 101 |
Format.eprintf "Launching analysis@.@?"; |
|
| 101 | 102 |
let new_e_salsa, e_val = |
| 102 | 103 |
Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv |
| 103 | 104 |
in |
| 105 |
Format.eprintf " Analysis done@.@?"; |
|
| 104 | 106 |
|
| 105 | 107 |
|
| 106 | 108 |
(* (\* Debug *\) *) |
| ... | ... | |
| 109 | 111 |
(* (Salsa.Print.printExpression new_e_salsa); *) |
| 110 | 112 |
(* (\* Debug *\) *) |
| 111 | 113 |
|
| 114 |
Format.eprintf " Computing range progress@.@?"; |
|
| 112 | 115 |
|
| 113 | 116 |
let old_val = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in |
| 114 | 117 |
let expr, expr_range = |
| ... | ... | |
| 119 | 122 |
); |
| 120 | 123 |
e_salsa, Some old_val |
| 121 | 124 |
) |
| 122 |
| true, false -> (
|
|
| 125 |
| false, true -> (
|
|
| 123 | 126 |
if !debug then Log.report ~level:2 (fun fmt -> |
| 124 | 127 |
Format.fprintf fmt "Improved!@ "; |
| 125 | 128 |
); |
| 126 | 129 |
new_e_salsa, Some e_val |
| 127 | 130 |
) |
| 128 |
| false, true -> Format.eprintf "CAREFUL --- new range is worse!. Restoring provided expression@ "; e_salsa, Some old_val |
|
| 129 |
|
|
| 130 |
| false, false -> |
|
| 131 |
Format.eprintf |
|
| 132 |
"Error; new range is not comparabe with old end. This should not happen!@.@?"; |
|
| 133 |
assert false |
|
| 131 |
| true, false -> Format.eprintf "CAREFUL --- new range is worse!. Restoring provided expression@ "; e_salsa, Some old_val |
|
| 132 |
|
|
| 133 |
| false, false -> ( |
|
| 134 |
Format.eprintf |
|
| 135 |
"Error; new range is not comparabe with old end. It may need some investigation!@.@?"; |
|
| 136 |
Format.eprintf "old: %a@.new: %a@.@?" |
|
| 137 |
RangesInt.pp_val old_val |
|
| 138 |
RangesInt.pp_val e_val; |
|
| 139 |
|
|
| 140 |
new_e_salsa, Some e_val |
|
| 141 |
(* assert false *) |
|
| 142 |
) |
|
| 134 | 143 |
in |
| 144 |
Format.eprintf " Computing range done@.@?"; |
|
| 145 |
|
|
| 135 | 146 |
if !debug then Log.report ~level:2 (fun fmt -> |
| 136 | 147 |
Format.fprintf fmt |
| 137 | 148 |
" @[<v>old_expr: @[<v 0>%s@ range: %a@]@ new_expr: @[<v 0>%s@ range: %a@]@ @]@ " |
| src/plugins/salsa/salsaDatatypes.ml | ||
|---|---|---|
| 112 | 112 |
| _ -> Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false |
| 113 | 113 |
*) |
| 114 | 114 |
let inject cst = match cst with |
| 115 |
| LT.Const_int(i) -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_float (float_of_int i))
|
|
| 115 |
| LT.Const_int(i) -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_int i)
|
|
| 116 | 116 |
| LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather |
| 117 | 117 |
compute the error associated to the float *) |
| 118 |
let f = float_of_string s in |
|
| 119 |
Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_float f) |
|
| 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) |
|
| 120 | 121 |
|
| 121 | 122 |
(* let r = Salsa.Prelude.r_of_f_aux r in *) |
| 122 | 123 |
(* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *) |
| ... | ... | |
| 128 | 129 |
(* Salsa.Builder.mk_cst (ST.I(r*.(1.-.epsilon_float),r*.(1.+.epsilon_float)),Float.ulp (ST.I(r,r))) *) |
| 129 | 130 |
| _ -> assert false |
| 130 | 131 |
|
| 131 |
let leq = Salsa.Float.feSseq
|
|
| 132 |
let leq = (* Salsa.Float.feSseq *) Salsa.Float.Domain.leq
|
|
| 132 | 133 |
end |
| 133 | 134 |
|
| 134 | 135 |
module RangesInt = Ranges (FloatIntSalsa) |
Also available in: Unified diff
More work on Salsa plugin